Merge pull request #7421 from esteffin/esteffin/add-cbmc-primitive-regression

Add cbmc primitive regression tests

Author: thomasspriggs

regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --no-simplify --no-propagation
 ^EXIT=10$

regression/cbmc-primitives/dynamic-object-02/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=10$

regression/cbmc-primitives/exists_memory_checks/negated_exists.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 negated_exists.c
 --pointer-check
 ^EXIT=0$

regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --no-simplify --no-propagation
 ^EXIT=10$

regression/cbmc-primitives/pointer-offset-01/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=10$

regression/cbmc-primitives/r_w_ok_bug/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check --no-simplify --no-propagation
 ^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*p1: FAILURE$

regression/cbmc-primitives/r_w_ok_valid_negated/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check --no-simplify --no-propagation
 ^EXIT=0$

regression/cbmc-primitives/same-object-03/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --no-simplify --no-propagation
 ^EXIT=0$

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1351,7 +1351,7 @@ static smt_termt convert_expr_to_smt(
     smt_bit_vector_theoryt::extract(offset_bits - 1, 0)(converted_expr);
   if(width > offset_bits)
   {
-    return smt_bit_vector_theoryt::zero_extend(width - offset_bits)(extract_op);
+    return smt_bit_vector_theoryt::sign_extend(width - offset_bits)(extract_op);
   }
   return extract_op;
 }

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1633,7 +1633,7 @@ TEST_CASE("pointer_offset_exprt to SMT conversion", "[core][smt2_incremental]")
   {
     const auto converted = test.convert(pointer_offset);
     const auto expected =
-      smt_bit_vector_theoryt::zero_extend(8)(smt_bit_vector_theoryt::extract(
+      smt_bit_vector_theoryt::sign_extend(8)(smt_bit_vector_theoryt::extract(
         55, 0)(smt_identifier_termt("foo", smt_bit_vector_sortt(64))));
     CHECK(converted == expected);
   }