Skip to content

Commit c19a933

Browse files
author
Enrico Steffinlongo
authored
Merge pull request #7909 from esteffin/esteffin/define-shadow-memory-primitives
Enable typechecking of shadow memory primitives
2 parents 10c4bca + b7ebd34 commit c19a933

File tree

16 files changed

+871
-4
lines changed

16 files changed

+871
-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/intrinsics_warnings1/intrinsics_warn.c

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
//
2+
// Created by Fotis Koutoulakis on 19/09/2023.
3+
//
4+
#include <assert.h>
5+
#include <stdio.h>
6+
7+
struct S
8+
{
9+
int i;
10+
int j;
11+
};
12+
13+
int main()
14+
{
15+
__CPROVER_field_decl_local("uninitialized", (char)0);
16+
__CPROVER_field_decl_global("uninitialized-global", (char)0);
17+
18+
struct S s;
19+
char a;
20+
21+
__CPROVER_set_field(&a, "uninitialized", 1);
22+
23+
assert(__CPROVER_get_field(&a, "uninitialized") == 1);
24+
25+
__CPROVER_set_field(&s, "uninitialized", 1);
26+
27+
assert(__CPROVER_get_field(&s, "uninitialized") == 1);
28+
assert(__CPROVER_get_field(&s.i, "uninitialized") == 1);
29+
assert(__CPROVER_get_field(&s.j, "uninitialized") == 1);
30+
31+
return 0;
32+
}

‎regression/cbmc-shadow-memory/intrinsics_warnings1/test.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
intrinsics_warn.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring
9+
WARNING: no body for function
10+
file intrinsics_warn.c line \d+ function main: function '__CPROVER_field_decl_global' is not declared
11+
file intrinsics_warn.c line \d+ function main: function '__CPROVER_field_decl_local' is not declared
12+
file intrinsics_warn.c line \d+ function main: function '__CPROVER_set_field' is not declared
13+
file intrinsics_warn.c line \d+ function main: function '__CPROVER_get_field' is not declared
14+
--
15+
This test is making sure that we don't get any of the log messages warning
16+
for the shadow memory intrinsics being undefined after the type check phase.

‎regression/cbmc-shadow-memory/intrinsics_warnings2/test.desc

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
typechecking_warning.c
3+
4+
^EXIT=6$
5+
^SIGNAL=0$
6+
^CONVERSION ERROR$
7+
file typechecking_warning\.c line \d function main: __CPROVER_field_decl_local argument 2 must be a byte-sized integer, but \(10ul\) has type `unsigned long int`
8+
--
9+
^warning: ignoring
10+
WARNING: no body for function
11+
file intrinsics_warn.c line \d+ function main: function '__CPROVER_field_decl_global' is not declared
12+
file intrinsics_warn.c line \d+ function main: function '__CPROVER_field_decl_local' is not declared
13+
file intrinsics_warn.c line \d+ function main: function '__CPROVER_set_field' is not declared
14+
file intrinsics_warn.c line \d+ function main: function '__CPROVER_get_field' is not declared
15+
--
16+
This test is part of a suite of tests we have for ensuring that the typechecker
17+
comes up with proper error messages in the case of shadow memory intrinsics
18+
failing the typechecking phase.

‎regression/cbmc-shadow-memory/intrinsics_warnings2/typechecking_warning.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
//
2+
// Created by Fotis Koutoulakis on 19/09/2023.
3+
//
4+
int main()
5+
{
6+
__CPROVER_field_decl_local("uninitialized", 10ul);
7+
8+
return 0;
9+
}

‎regression/cbmc-shadow-memory/intrinsics_warnings3/test.desc

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
typechecking_warning.c
3+
4+
^EXIT=6$
5+
^SIGNAL=0$
6+
^CONVERSION ERROR$
7+
file typechecking_warning\.c line \d function main: __CPROVER_field_decl_local takes exactly 2 arguments, but 1 were provided
8+
--
9+
^warning: ignoring
10+
WARNING: no body for function
11+
file intrinsics_warn.c line \d+ function main: function '__CPROVER_field_decl_global' is not declared
12+
file intrinsics_warn.c line \d+ function main: function '__CPROVER_field_decl_local' is not declared
13+
file intrinsics_warn.c line \d+ function main: function '__CPROVER_set_field' is not declared
14+
file intrinsics_warn.c line \d+ function main: function '__CPROVER_get_field' is not declared
15+
--
16+
This test is part of a suite of tests we have for ensuring that the typechecker
17+
comes up with proper error messages in the case of shadow memory intrinsics
18+
failing the typechecking phase.

‎regression/cbmc-shadow-memory/intrinsics_warnings3/typechecking_warning.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
//
2+
// Created by Fotis Koutoulakis on 19/09/2023.
3+
//
4+
int main()
5+
{
6+
__CPROVER_field_decl_local("uninitialized");
7+
8+
return 0;
9+
}

‎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)