C++: Add a new 'Location.isBefore' predicate that also considers columns.

This commit is contained in:
Mathias Vorreiter Pedersen
2022-03-22 11:49:57 +00:00
parent c6c3206031
commit 93346a574f
3 changed files with 26 additions and 13 deletions

View File

@@ -73,8 +73,24 @@ class Location extends @location {
/** Holds if `this` comes on a line strictly before `l`. */
pragma[inline]
predicate isBefore(Location l) {
this.getFile() = l.getFile() and this.getEndLine() < l.getStartLine()
predicate isBefore(Location l) { isBefore(l, false) }
/**
* Holds if `this` comes strictly before `l`. The boolean `sameLine` is
* true if `l` is on the same line as `this`, but starts at a later column.
* Otherwise, `sameLine` is false.
*/
pragma[inline]
predicate isBefore(Location l, boolean sameLine) {
this.getFile() = l.getFile() and
(
sameLine = false and
this.getEndLine() < l.getStartLine()
or
sameLine = true and
this.getEndLine() = l.getStartLine() and
this.getEndColumn() < l.getStartColumn()
)
}
/** Holds if location `l` is completely contained within this one. */

View File

@@ -349,7 +349,7 @@ Instruction getInstructionBackEdgeSuccessor(Instruction instruction, EdgeKind ki
/** Holds if `goto` jumps strictly forward in the program text. */
private predicate isStrictlyForwardGoto(GotoStmt goto) {
goto.getLocation().isBefore(goto.getTarget().getLocation())
goto.getLocation().isBefore(goto.getTarget().getLocation(), _)
}
Locatable getInstructionAst(TStageInstruction instr) {