module author Paolo Masci
 *  date copyright import { Diagnostic , DiagnosticSeverity , Range , Position } from 'vscode-languageserver' ; import * as utils from '../common/languageUtils' ; /**
 * Linter heuristics
 */ const linter = [ { note : "group 1 is the annotation, group 2 is the type/datatype definition" , regexp : /(\%+\s*.+\s+)?(\w+\s*:\s*(?:\bTYPE\b|\bDATATYPE\b))/gi , msg : "Type definitions should be preceeded by proper documentation" } ] ; /**
 * PVS linter class, identifies anti-patterns, i.e., pieces of code that should be amended
 */ export class PvsLinter { provideDiagnostics ( document ) { let diag = [ ] ; let match = null ; const content = document . txt . replace ( utils . commentRegexp , "" ) ; for ( let i = 0 ; i < linter . length ; i ++ ) { while ( match = linter [ i ] . regexp . exec ( content ) ) { if ( match . length > 2 && ( ! match [ 1 ] || match [ 1 ] === "" ) ) { const lines = content . substring ( 0 , match . index ) . split ( "\n" ) ; const line = lines . length - 1 ; const character = lines [ line ] . length - 1 ; let position = { line , character } ; let range = { start : position , end : { line : position . line , character : position . character + match [ 2 ] . length } } ; diag . push ( { severity : DiagnosticSeverity . Warning , range : range , message : linter [ i ] . msg , source : "PVS Linter" } ) ; } } } return diag ; } }