From de9340c4b6fad5f03f658d39a1f8c8961713b51b Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Sun, 16 Jul 2023 18:40:57 +0100 Subject: [PATCH 1/3] Activate all struct tests from regression/cbmc/ --- regression/cbmc/Anonymous_Struct1/test.desc | 2 +- regression/cbmc/Anonymous_Struct2/test.desc | 2 +- regression/cbmc/Anonymous_Struct3/test.desc | 2 +- regression/cbmc/Struct_Array1/test.desc | 2 +- regression/cbmc/Struct_Bytewise1/test.desc | 2 +- regression/cbmc/Struct_Bytewise2/test.desc | 2 +- regression/cbmc/Struct_Initialization1/test.desc | 2 +- regression/cbmc/Struct_Initialization10/test.desc | 2 +- regression/cbmc/Struct_Initialization2/test.desc | 2 +- regression/cbmc/Struct_Initialization3/test.desc | 2 +- regression/cbmc/Struct_Initialization4/test.desc | 2 +- regression/cbmc/Struct_Initialization5/test.desc | 2 +- regression/cbmc/Struct_Initialization6/test.desc | 2 +- regression/cbmc/Struct_Initialization7/test.desc | 2 +- regression/cbmc/Struct_Initialization8/test.desc | 2 +- regression/cbmc/Struct_Initialization9/test.desc | 2 +- regression/cbmc/Struct_Padding1/test.desc | 2 +- regression/cbmc/Struct_Pointer1/test.desc | 2 +- regression/cbmc/Struct_Pointer2/test.desc | 2 +- regression/cbmc/Struct_Pointer3/test.desc | 2 +- regression/cbmc/Struct_Pointer_Array1/test.desc | 2 +- regression/cbmc/Struct_Propagation1/test.desc | 2 +- regression/cbmc/struct1/test.desc | 2 +- regression/cbmc/struct10/test.desc | 2 +- regression/cbmc/struct11/test.desc | 2 +- regression/cbmc/struct12/test.desc | 2 +- regression/cbmc/struct13/test.desc | 2 +- regression/cbmc/struct14/test.desc | 2 +- regression/cbmc/struct15/test.desc | 2 +- regression/cbmc/struct16/test.desc | 2 +- regression/cbmc/struct17/test.desc | 2 +- regression/cbmc/struct3/test.desc | 2 +- regression/cbmc/struct4/test.desc | 2 +- regression/cbmc/struct6/test.desc | 2 +- regression/cbmc/struct7/test.desc | 2 +- regression/cbmc/struct8/test.desc | 2 +- regression/cbmc/struct9/test.desc | 2 +- 37 files changed, 37 insertions(+), 37 deletions(-) diff --git a/regression/cbmc/Anonymous_Struct1/test.desc b/regression/cbmc/Anonymous_Struct1/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Anonymous_Struct1/test.desc +++ b/regression/cbmc/Anonymous_Struct1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Anonymous_Struct2/test.desc b/regression/cbmc/Anonymous_Struct2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Anonymous_Struct2/test.desc +++ b/regression/cbmc/Anonymous_Struct2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Anonymous_Struct3/test.desc b/regression/cbmc/Anonymous_Struct3/test.desc index 7057e2afbe7..86980b336e4 100644 --- a/regression/cbmc/Anonymous_Struct3/test.desc +++ b/regression/cbmc/Anonymous_Struct3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c -win32 ^EXIT=0$ diff --git a/regression/cbmc/Struct_Array1/test.desc b/regression/cbmc/Struct_Array1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Array1/test.desc +++ b/regression/cbmc/Struct_Array1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Bytewise1/test.desc b/regression/cbmc/Struct_Bytewise1/test.desc index 03ad7634d7c..4452a33cdc0 100644 --- a/regression/cbmc/Struct_Bytewise1/test.desc +++ b/regression/cbmc/Struct_Bytewise1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend struct_bytewise.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Bytewise2/test.desc b/regression/cbmc/Struct_Bytewise2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Bytewise2/test.desc +++ b/regression/cbmc/Struct_Bytewise2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Initialization1/test.desc b/regression/cbmc/Struct_Initialization1/test.desc index 0797c56a2cc..34817532309 100644 --- a/regression/cbmc/Struct_Initialization1/test.desc +++ b/regression/cbmc/Struct_Initialization1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Initialization10/test.desc b/regression/cbmc/Struct_Initialization10/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Initialization10/test.desc +++ b/regression/cbmc/Struct_Initialization10/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Initialization2/test.desc b/regression/cbmc/Struct_Initialization2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Initialization2/test.desc +++ b/regression/cbmc/Struct_Initialization2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Initialization3/test.desc b/regression/cbmc/Struct_Initialization3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Initialization3/test.desc +++ b/regression/cbmc/Struct_Initialization3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Initialization4/test.desc b/regression/cbmc/Struct_Initialization4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Initialization4/test.desc +++ b/regression/cbmc/Struct_Initialization4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Initialization5/test.desc b/regression/cbmc/Struct_Initialization5/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Initialization5/test.desc +++ b/regression/cbmc/Struct_Initialization5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Initialization6/test.desc b/regression/cbmc/Struct_Initialization6/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Initialization6/test.desc +++ b/regression/cbmc/Struct_Initialization6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Initialization7/test.desc b/regression/cbmc/Struct_Initialization7/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Initialization7/test.desc +++ b/regression/cbmc/Struct_Initialization7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Initialization8/test.desc b/regression/cbmc/Struct_Initialization8/test.desc index aea17ee4da8..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Initialization8/test.desc +++ b/regression/cbmc/Struct_Initialization8/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Initialization9/test.desc b/regression/cbmc/Struct_Initialization9/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Initialization9/test.desc +++ b/regression/cbmc/Struct_Initialization9/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Padding1/test.desc b/regression/cbmc/Struct_Padding1/test.desc index 35cc9d3cd74..0c98ed635a3 100644 --- a/regression/cbmc/Struct_Padding1/test.desc +++ b/regression/cbmc/Struct_Padding1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.i --32 ^EXIT=0$ diff --git a/regression/cbmc/Struct_Pointer1/test.desc b/regression/cbmc/Struct_Pointer1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Pointer1/test.desc +++ b/regression/cbmc/Struct_Pointer1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Pointer2/test.desc b/regression/cbmc/Struct_Pointer2/test.desc index 39c491ba8bb..86726dd3c44 100644 --- a/regression/cbmc/Struct_Pointer2/test.desc +++ b/regression/cbmc/Struct_Pointer2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/Struct_Pointer3/test.desc b/regression/cbmc/Struct_Pointer3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Pointer3/test.desc +++ b/regression/cbmc/Struct_Pointer3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Pointer_Array1/test.desc b/regression/cbmc/Struct_Pointer_Array1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Pointer_Array1/test.desc +++ b/regression/cbmc/Struct_Pointer_Array1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/Struct_Propagation1/test.desc b/regression/cbmc/Struct_Propagation1/test.desc index 42e6505e2d3..25707ea2b5c 100644 --- a/regression/cbmc/Struct_Propagation1/test.desc +++ b/regression/cbmc/Struct_Propagation1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --unwind 5 ^EXIT=0$ diff --git a/regression/cbmc/struct1/test.desc b/regression/cbmc/struct1/test.desc index 83b8819429a..4de445f0439 100644 --- a/regression/cbmc/struct1/test.desc +++ b/regression/cbmc/struct1/test.desc @@ -1,4 +1,4 @@ -CORE gcc-only +CORE gcc-only new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/struct10/test.desc b/regression/cbmc/struct10/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/struct10/test.desc +++ b/regression/cbmc/struct10/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/struct11/test.desc b/regression/cbmc/struct11/test.desc index 8a897dcc15e..667664c6acf 100644 --- a/regression/cbmc/struct11/test.desc +++ b/regression/cbmc/struct11/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/struct12/test.desc b/regression/cbmc/struct12/test.desc index d678193e09e..41402fa5070 100644 --- a/regression/cbmc/struct12/test.desc +++ b/regression/cbmc/struct12/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/struct13/test.desc b/regression/cbmc/struct13/test.desc index 42120d278a5..5d3b63b4691 100644 --- a/regression/cbmc/struct13/test.desc +++ b/regression/cbmc/struct13/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/struct14/test.desc b/regression/cbmc/struct14/test.desc index b69d909607e..e9858d2ce80 100644 --- a/regression/cbmc/struct14/test.desc +++ b/regression/cbmc/struct14/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=10$ diff --git a/regression/cbmc/struct15/test.desc b/regression/cbmc/struct15/test.desc index 81a142d267f..b624eba8b29 100644 --- a/regression/cbmc/struct15/test.desc +++ b/regression/cbmc/struct15/test.desc @@ -1,4 +1,4 @@ -CORE smt-backend +CORE smt-backend new-smt-backend main.c --trace --z3 ^EXIT=0$ diff --git a/regression/cbmc/struct16/test.desc b/regression/cbmc/struct16/test.desc index 9927cd18857..3d4de29922f 100644 --- a/regression/cbmc/struct16/test.desc +++ b/regression/cbmc/struct16/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/struct17/test.desc b/regression/cbmc/struct17/test.desc index 659a36aac28..624edd88c09 100644 --- a/regression/cbmc/struct17/test.desc +++ b/regression/cbmc/struct17/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/struct3/test.desc b/regression/cbmc/struct3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/struct3/test.desc +++ b/regression/cbmc/struct3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/struct4/test.desc b/regression/cbmc/struct4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/struct4/test.desc +++ b/regression/cbmc/struct4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/struct6/test.desc b/regression/cbmc/struct6/test.desc index da239c1965b..6e36fa13566 100644 --- a/regression/cbmc/struct6/test.desc +++ b/regression/cbmc/struct6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --bounds-check --pointer-check ^EXIT=0$ diff --git a/regression/cbmc/struct7/test.desc b/regression/cbmc/struct7/test.desc index 96c9b4bcd7b..5821c3e2820 100644 --- a/regression/cbmc/struct7/test.desc +++ b/regression/cbmc/struct7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc/struct8/test.desc b/regression/cbmc/struct8/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/struct8/test.desc +++ b/regression/cbmc/struct8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/struct9/test.desc b/regression/cbmc/struct9/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/struct9/test.desc +++ b/regression/cbmc/struct9/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ From 7de085d17742ec5520ff706d128dc79871eeeb9b Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Sun, 16 Jul 2023 21:26:33 +0100 Subject: [PATCH 2/3] Add test for address of member --- .../address_of_struct_member/address_of.c | 19 +++++++++++++++++++ .../cbmc/address_of_struct_member/test.desc | 9 +++++++++ 2 files changed, 28 insertions(+) create mode 100644 regression/cbmc/address_of_struct_member/address_of.c create mode 100644 regression/cbmc/address_of_struct_member/test.desc diff --git a/regression/cbmc/address_of_struct_member/address_of.c b/regression/cbmc/address_of_struct_member/address_of.c new file mode 100644 index 00000000000..99787968b11 --- /dev/null +++ b/regression/cbmc/address_of_struct_member/address_of.c @@ -0,0 +1,19 @@ +struct expr +{ + int line; + char comment; +}; + +int main(int argc, char *argv[]) +{ + struct expr var_expr = {42, 'a'}; + struct expr other_expr = {34, 'b'}; + unsigned int nondet; + int *ref; + if(nondet) + ref = &var_expr.line; + else + ref = &other_expr.line; + __CPROVER_assert(*ref != 34, "expected failure: ref == 34"); + return 0; +} diff --git a/regression/cbmc/address_of_struct_member/test.desc b/regression/cbmc/address_of_struct_member/test.desc new file mode 100644 index 00000000000..d5dc9a41012 --- /dev/null +++ b/regression/cbmc/address_of_struct_member/test.desc @@ -0,0 +1,9 @@ +CORE new-smt-backend +address_of.c + +\[main\.assertion\.1\] line \d+ expected failure: ref == 34: FAILURE +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- From eadb111a06c6de34b17dcc9d1dff703326f02890 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 17 Jul 2023 10:43:58 +0100 Subject: [PATCH 3/3] Add regression test for nested struct member --- .../cbmc/Struct_Initialization5/test.desc | 2 +- .../address_of_rec.c | 26 +++++++++++++++++++ .../address_of_struct_member_rec/test.desc | 9 +++++++ regression/cbmc/struct16/test.desc | 2 +- 4 files changed, 37 insertions(+), 2 deletions(-) create mode 100644 regression/cbmc/address_of_struct_member_rec/address_of_rec.c create mode 100644 regression/cbmc/address_of_struct_member_rec/test.desc diff --git a/regression/cbmc/Struct_Initialization5/test.desc b/regression/cbmc/Struct_Initialization5/test.desc index f4cb0fa5f29..9efefbc7362 100644 --- a/regression/cbmc/Struct_Initialization5/test.desc +++ b/regression/cbmc/Struct_Initialization5/test.desc @@ -1,4 +1,4 @@ -CORE new-smt-backend +CORE main.c ^EXIT=0$ diff --git a/regression/cbmc/address_of_struct_member_rec/address_of_rec.c b/regression/cbmc/address_of_struct_member_rec/address_of_rec.c new file mode 100644 index 00000000000..6480c8f482a --- /dev/null +++ b/regression/cbmc/address_of_struct_member_rec/address_of_rec.c @@ -0,0 +1,26 @@ +struct aux +{ + char comment; +}; + +struct expr +{ + int line; + struct aux *info; +}; + +int main(void) +{ + struct aux info1 = {'a'}; + struct aux info2 = {'b'}; + struct expr var_expr = {42, &info1}; + struct expr other_expr = {34, &info2}; + unsigned int nondet; + char *ref; + if(nondet) + ref = &var_expr.info->comment; + else + ref = &other_expr.info->comment; + __CPROVER_assert(*ref != 'b', "expected failure: ref == 'b'"); + return 0; +} diff --git a/regression/cbmc/address_of_struct_member_rec/test.desc b/regression/cbmc/address_of_struct_member_rec/test.desc new file mode 100644 index 00000000000..a0ab293013e --- /dev/null +++ b/regression/cbmc/address_of_struct_member_rec/test.desc @@ -0,0 +1,9 @@ +CORE new-smt-backend +address_of_rec.c + +\[main\.assertion\.1\] line \d+ expected failure: ref == 'b': FAILURE +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/regression/cbmc/struct16/test.desc b/regression/cbmc/struct16/test.desc index 3d4de29922f..9927cd18857 100644 --- a/regression/cbmc/struct16/test.desc +++ b/regression/cbmc/struct16/test.desc @@ -1,4 +1,4 @@ -CORE new-smt-backend +CORE main.c ^VERIFICATION SUCCESSFUL$