From 00e03cb4c1c074ba4323afd4a4833da4b2329607 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 31 May 2023 17:26:46 +0100 Subject: [PATCH] Enable SMT solver tests fixed by rudimentary struct support These tests now pass due to the functionality added in PR7740. --- regression/cbmc/Endianness7/test.desc | 2 +- regression/cbmc/Malloc13/test.desc | 2 +- regression/cbmc/Malloc23/test.desc | 2 +- regression/cbmc/String_Abstraction24/test.desc | 2 +- regression/cbmc/equality_through_array_of_struct1/test.desc | 2 +- regression/cbmc/equality_through_array_of_struct2/test.desc | 2 +- regression/cbmc/equality_through_array_of_struct3/test.desc | 2 +- regression/cbmc/equality_through_array_of_struct4/test.desc | 2 +- regression/cbmc/offsetof1/test.desc | 2 +- 9 files changed, 9 insertions(+), 9 deletions(-) diff --git a/regression/cbmc/Endianness7/test.desc b/regression/cbmc/Endianness7/test.desc index 54056d719c9..a1d9aa1f8a4 100644 --- a/regression/cbmc/Endianness7/test.desc +++ b/regression/cbmc/Endianness7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --big-endian --no-simplify ^EXIT=0$ diff --git a/regression/cbmc/Malloc13/test.desc b/regression/cbmc/Malloc13/test.desc index f3145b289ad..ccde4872657 100644 --- a/regression/cbmc/Malloc13/test.desc +++ b/regression/cbmc/Malloc13/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --string-abstraction ^EXIT=0$ diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc index 39d94af76fd..afc24e98c7c 100644 --- a/regression/cbmc/Malloc23/test.desc +++ b/regression/cbmc/Malloc23/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --pointer-check ^EXIT=10$ diff --git a/regression/cbmc/String_Abstraction24/test.desc b/regression/cbmc/String_Abstraction24/test.desc index 2c2667887f0..f3e2764ae85 100644 --- a/regression/cbmc/String_Abstraction24/test.desc +++ b/regression/cbmc/String_Abstraction24/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c --string-abstraction ^VERIFICATION FAILED$ diff --git a/regression/cbmc/equality_through_array_of_struct1/test.desc b/regression/cbmc/equality_through_array_of_struct1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/equality_through_array_of_struct1/test.desc +++ b/regression/cbmc/equality_through_array_of_struct1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/equality_through_array_of_struct2/test.desc b/regression/cbmc/equality_through_array_of_struct2/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/equality_through_array_of_struct2/test.desc +++ b/regression/cbmc/equality_through_array_of_struct2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/equality_through_array_of_struct3/test.desc b/regression/cbmc/equality_through_array_of_struct3/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/equality_through_array_of_struct3/test.desc +++ b/regression/cbmc/equality_through_array_of_struct3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/equality_through_array_of_struct4/test.desc b/regression/cbmc/equality_through_array_of_struct4/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/equality_through_array_of_struct4/test.desc +++ b/regression/cbmc/equality_through_array_of_struct4/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$ diff --git a/regression/cbmc/offsetof1/test.desc b/regression/cbmc/offsetof1/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/offsetof1/test.desc +++ b/regression/cbmc/offsetof1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$