Skip to content

Commit b7ebd34

Browse files
author
Enrico Steffinlongo
committed
Fixed SM failing regressions tests.
Fixed SM failing regression tests due to better error messaging on typecheck.
1 parent 0e58b9b commit b7ebd34

File tree

4 files changed

+8
-4
lines changed

4 files changed

+8
-4
lines changed

regression/cbmc-shadow-memory/declarations1/test_bad1.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,8 @@ bad1.c
33
--function bad_declaration1 --verbosity 10
44
^EXIT=6$
55
^SIGNAL=0$
6-
^A shadow memory field must not be larger than 8 bits.
6+
^file bad1\.c line 3 function bad_declaration1: __CPROVER_field_decl_local argument 2 must be a byte-sized integer, but \(\(signed int\)0\) has type `signed int`
7+
^CONVERSION ERROR
78
--
89
--
910
Test that a shadow memory declaration of a too large type is rejected.

regression/cbmc-shadow-memory/declarations1/test_bad2.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,8 @@ bad2.c
33
--function bad_declaration2 --verbosity 10
44
^EXIT=6$
55
^SIGNAL=0$
6-
^A shadow memory field must be of a bitvector type.
6+
^file bad2\.c line 7 function bad_declaration2: __CPROVER_field_decl_global argument 2 must be a byte-sized integer, but \(s\) has type `struct STRUCT`
7+
^CONVERSION ERROR
78
--
89
--
910
Test that a shadow memory declaration of a non-bitvector type is rejected.

regression/cbmc-shadow-memory/void-ptr-param-get1/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ main.c
33

44
^EXIT=6$
55
^SIGNAL=0$
6-
Shadow memory: cannot get shadow memory via type void\* for f_void_ptr::s
6+
^file main\.c line 12 function f_void_ptr: __CPROVER_get_field argument 1 must be a non-void pointer, but \(s\) has type `void \*`. Insert a cast to the type that you want to access\.
7+
CONVERSION ERROR
78
--
89
^warning: ignoring

regression/cbmc-shadow-memory/void-ptr-param-set1/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ main.c
33

44
^EXIT=6$
55
^SIGNAL=0$
6-
Shadow memory: cannot set shadow memory via type void\* for f_void_ptr::s
6+
^file main\.c line 12 function f_void_ptr: __CPROVER_set_field argument 1 must be a non-void pointer, but \(s\) has type `void \*`\. Insert a cast to the type that you want to access\.
7+
^CONVERSION ERROR
78
--
89
^warning: ignoring

0 commit comments

Comments
 (0)