File tree 3 files changed +5
-5
lines changed
variable-sensitivity-dependence-graph-merge
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
5
5
^EXIT=0$
6
6
^SIGNAL=0$
7
7
// 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 \]
11
11
--
12
12
// The __CPROVER__start function must not have a control dependency on anything
13
13
Function: __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
5
5
^EXIT=0$
6
6
^SIGNAL=0$
7
7
Control 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;
9
9
10
10
--
11
11
^warning: ignoring
Original file line number Diff line number Diff line change 3
3
--dependence-graph-vs --structs --arrays --verify
4
4
EXIT=0
5
5
SIGNAL=0
6
- ^\[main.assertion.1\] file .* function main, idx== 1: Unknown$
6
+ ^\[main.assertion.1\] file .* function main, s_str. idx > 1: Unknown$
7
7
--
You can’t perform that action at this time.
0 commit comments