@@ -30,63 +30,62 @@ class Location = S::Location;
3030
3131class Node = Cfg:: ControlFlowNode ;
3232
33- module CfgInput implements InputSig< Location > {
34- class AstNode = ControlFlowElement ;
35-
36- class Completion = C:: Completion ;
37-
38- predicate completionIsNormal = C:: completionIsNormal / 1 ;
39-
40- predicate completionIsSimple = C:: completionIsSimple / 1 ;
41-
42- predicate completionIsValidFor = C:: completionIsValidFor / 2 ;
43-
44- /** An AST node with an associated control-flow graph. */
45- class CfgScope extends S:: Locatable instanceof Impl:: CfgScope:: Range_ { }
46-
47- CfgScope getCfgScope ( AstNode n ) { result = scopeOfAst ( n .asAstNode ( ) ) }
48-
49- class SplitKindBase = Splitting:: TSplitKind ;
50-
51- class Split = Splitting:: Split ;
52-
53- class SuccessorType = Cfg:: SuccessorType ;
54-
55- /** Gets a successor type that matches completion `c`. */
56- SuccessorType getAMatchingSuccessorType ( Completion c ) { result = c .getAMatchingSuccessorType ( ) }
57-
58- /**
59- * Hold if `c` represents simple (normal) evaluation of a statement or an
60- * expression.
61- */
62- predicate successorTypeIsSimple ( SuccessorType t ) {
63- t instanceof Cfg:: SuccessorTypes:: NormalSuccessor
64- }
65-
66- /** Holds if `t` is an abnormal exit type out of a CFG scope. */
67- predicate isAbnormalExitType ( SuccessorType t ) {
68- t instanceof Cfg:: SuccessorTypes:: ExceptionSuccessor
69- }
70-
71- /** Hold if `t` represents a conditional successor type. */
72- predicate successorTypeIsCondition ( SuccessorType t ) {
73- t instanceof Cfg:: SuccessorTypes:: BooleanSuccessor or
74- t instanceof Cfg:: SuccessorTypes:: BreakSuccessor or
75- t instanceof Cfg:: SuccessorTypes:: ContinueSuccessor or
76- t instanceof Cfg:: SuccessorTypes:: MatchingSuccessor or
77- t instanceof Cfg:: SuccessorTypes:: EmptinessSuccessor
78- }
79-
80- /** Holds if `first` is first executed when entering `scope`. */
81- predicate scopeFirst ( CfgScope scope , AstNode first ) {
82- scope .( Impl:: CfgScope:: Range_ ) .entry ( first )
83- }
84-
85- /** Holds if `scope` is exited when `last` finishes with completion `c`. */
86- predicate scopeLast ( CfgScope scope , AstNode last , Completion c ) {
87- scope .( Impl:: CfgScope:: Range_ ) .exit ( last , c )
88- }
89- }
90-
91- module CfgImpl = Make< Location , CfgInput > ;
92-
33+ module CfgInput implements InputSig< Location > {
34+ class AstNode = ControlFlowElement ;
35+
36+ class Completion = C:: Completion ;
37+
38+ predicate completionIsNormal = C:: completionIsNormal / 1 ;
39+
40+ predicate completionIsSimple = C:: completionIsSimple / 1 ;
41+
42+ predicate completionIsValidFor = C:: completionIsValidFor / 2 ;
43+
44+ /** An AST node with an associated control-flow graph. */
45+ class CfgScope extends S:: Locatable instanceof Impl:: CfgScope:: Range_ { }
46+
47+ CfgScope getCfgScope ( AstNode n ) { result = scopeOfAst ( n .asAstNode ( ) ) }
48+
49+ class SplitKindBase = Splitting:: TSplitKind ;
50+
51+ class Split = Splitting:: Split ;
52+
53+ class SuccessorType = Cfg:: SuccessorType ;
54+
55+ /** Gets a successor type that matches completion `c`. */
56+ SuccessorType getAMatchingSuccessorType ( Completion c ) { result = c .getAMatchingSuccessorType ( ) }
57+
58+ /**
59+ * Hold if `c` represents simple (normal) evaluation of a statement or an
60+ * expression.
61+ */
62+ predicate successorTypeIsSimple ( SuccessorType t ) {
63+ t instanceof Cfg:: SuccessorTypes:: NormalSuccessor
64+ }
65+
66+ /** Holds if `t` is an abnormal exit type out of a CFG scope. */
67+ predicate isAbnormalExitType ( SuccessorType t ) {
68+ t instanceof Cfg:: SuccessorTypes:: ExceptionSuccessor
69+ }
70+
71+ /** Hold if `t` represents a conditional successor type. */
72+ predicate successorTypeIsCondition ( SuccessorType t ) {
73+ t instanceof Cfg:: SuccessorTypes:: BooleanSuccessor or
74+ t instanceof Cfg:: SuccessorTypes:: BreakSuccessor or
75+ t instanceof Cfg:: SuccessorTypes:: ContinueSuccessor or
76+ t instanceof Cfg:: SuccessorTypes:: MatchingSuccessor or
77+ t instanceof Cfg:: SuccessorTypes:: EmptinessSuccessor
78+ }
79+
80+ /** Holds if `first` is first executed when entering `scope`. */
81+ predicate scopeFirst ( CfgScope scope , AstNode first ) {
82+ scope .( Impl:: CfgScope:: Range_ ) .entry ( first )
83+ }
84+
85+ /** Holds if `scope` is exited when `last` finishes with completion `c`. */
86+ predicate scopeLast ( CfgScope scope , AstNode last , Completion c ) {
87+ scope .( Impl:: CfgScope:: Range_ ) .exit ( last , c )
88+ }
89+ }
90+
91+ module CfgImpl = Make< Location , CfgInput > ;
0 commit comments