Skip to content

Commit 0624b69

Browse files
committed
Fixing regression test.
1 parent 5ebd8ba commit 0624b69

File tree

3 files changed

+10
-5
lines changed

3 files changed

+10
-5
lines changed
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
CORE
22
test.c
33
--no-simplify --unwind 300 --object-bits 8
4+
^EXIT=6$
5+
^SIGNAL=0$
46
too many addressed objects
5-
--
7+
--

regression/cbmc/realloc3/test.desc

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,12 @@
11
CORE
22
main.c
33

4-
^EXIT=0$
4+
^EXIT=6$
55
^SIGNAL=0$
6-
^VERIFICATION SUCCESSFUL$
6+
pointer handling for concurrency is unsound
77
--
88
^warning: ignoring
9+
--
10+
The test uses "__CPROVER_ASYNC_1:" and the async-called function foo
11+
does pointer operations over allocated memory - which is not handled sound
12+
way in CBMC.

regression/strings-smoke-tests/java_format/test.desc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,4 @@ test.class
55
^SIGNAL=0$
66
^\[.*assertion.1\].* line 6.* SUCCESS$
77
^\[.*assertion.2\].* line 7.* FAILURE$
8-
--
9-
^ignoring
8+
--

0 commit comments

Comments
 (0)