File tree Expand file tree Collapse file tree 3 files changed +5
-5
lines changed
variable-sensitivity-dependence-graph-merge Expand file tree Collapse file tree 3 files changed +5
-5
lines changed Original file line number Diff line number Diff line change @@ -5,9 +5,9 @@ activate-multi-line-match
55^EXIT=0$
66^SIGNAL=0$
77// The function entry points shall have a control dependency on the function call
8- Function: main\n.*\n.*\n.*\nControl dependencies: [0-9]+ \[CALL \]
9- Function: func\n.*\n.*\n.*\nControl dependencies: [0-9]+ \[CALL \]
10- Function: __CPROVER_initialize\n.*\n.*\n.*\nControl dependencies: [0-9]+ \[CALL \]
8+ Function: main\n.*\n.*\n.*\nControl dependencies: [0-9]+ \[UNCONDITIONAL \]
9+ Function: func\n.*\n.*\n.*\nControl dependencies: [0-9]+ \[UNCONDITIONAL \]
10+ Function: __CPROVER_initialize\n.*\n.*\n.*\nControl dependencies: [0-9]+ \[UNCONDITIONAL \]
1111--
1212// The __CPROVER__start function must not have a control dependency on anything
1313Function: __CPROVER__start\n.*\n.*\n.*\nControl dependencies: [0-9]+
Original file line number Diff line number Diff line change @@ -5,7 +5,7 @@ activate-multi-line-match
55^EXIT=0$
66^SIGNAL=0$
77Control dependencies: [0-9]+ \[TRUE\]\n.*\n.*\n\s+a = 1;
8- Control dependencies: [0-9]+ \[CALL \]\n.*\n.*\n\s+a = 2;
8+ Control dependencies: [0-9]+ \[UNCONDITIONAL \]\n.*\n.*\n\s+a = 2;
99
1010--
1111^warning: ignoring
Original file line number Diff line number Diff line change 33--dependence-graph-vs --structs --arrays --verify
44EXIT=0
55SIGNAL=0
6- ^\[main.assertion.1\] file .* function main, idx== 1: Unknown$
6+ ^\[main.assertion.1\] file .* function main, s_str. idx > 1: Unknown$
77--
You can’t perform that action at this time.
0 commit comments