File tree Expand file tree Collapse file tree 6 files changed +0
-12
lines changed
assigns_validity_pointer_01
assigns_validity_pointer_02
assigns_validity_pointer_04
history-pointer-enforce-01
history-pointer-enforce-02
history-pointer-enforce-08 Expand file tree Collapse file tree 6 files changed +0
-12
lines changed Original file line number Diff line number Diff line change @@ -16,9 +16,6 @@ ASSUME .*::tmp_if_expr\$\d
16
16
IF ¬\(z ≠ NULL\) THEN GOTO \d
17
17
ASSIGN .*::tmp_if_expr\$\d := \(\*z = 7 \? true : false\)
18
18
ASSUME .*::tmp_if_expr\$\d
19
- // foo
20
- ASSUME \*.*::tmp_cc\$\d > 0
21
- ASSERT \*.*::tmp_cc\$\d = 3
22
19
--
23
20
\[3\] file main\.c line 6 assertion: FAILURE
24
21
--
Original file line number Diff line number Diff line change 5
5
^SIGNAL=0$
6
6
^VERIFICATION SUCCESSFUL$
7
7
//^([foo\.1] line 15 assertion: FAILURE)
8
- // foo
9
- ASSUME \*.*::tmp_cc\$\d > 0
10
- ASSERT \*.*::tmp_cc\$\d = 3
11
8
--
12
9
\[foo\.1\] line 24 assertion: FAILURE
13
10
\[foo\.3\] line 27 assertion: FAILURE
Original file line number Diff line number Diff line change @@ -11,9 +11,6 @@ ASSIGN goto_convertt::tmp_if_expr := \(\*foo::1::y = 5 \? true : false\)
11
11
ASSUME .*::tmp_if_expr
12
12
// baz
13
13
ASSUME \*z = 7
14
- // foo
15
- ASSUME \*.*::tmp_cc\$\d > 0
16
- ASSERT \*.*::tmp_cc\$\d = 3
17
14
--
18
15
--
19
16
Verification:
Original file line number Diff line number Diff line change 4
4
^EXIT=0$
5
5
^SIGNAL=0$
6
6
^VERIFICATION SUCCESSFUL$
7
- ASSERT \*.*::tmp_cc\$\d = .*::tmp_cc\$\d \+ 5
8
7
--
9
8
--
10
9
Verification:
Original file line number Diff line number Diff line change 4
4
^EXIT=10$
5
5
^SIGNAL=0$
6
6
^VERIFICATION FAILED$
7
- ASSERT \*.*::tmp_cc\$\d < .*::tmp_cc\$\d \+ 5
8
7
--
9
8
--
10
9
Verification:
Original file line number Diff line number Diff line change 4
4
^EXIT=0$
5
5
^SIGNAL=0$
6
6
^VERIFICATION SUCCESSFUL$
7
- ASSERT \*\(.*::tmp_cc\$\d\.y\) = .*::tmp_cc\$\d \+ 5
8
7
--
9
8
--
10
9
Verification:
You can’t perform that action at this time.
0 commit comments