fix: add missing integer casts and operations

adds:
integer->bool cast
bool -> integer cast
integer minus operation

Author: polgreen

regression/CMakeLists.txt

@@ -14,10 +14,10 @@ endmacro(add_test_pl_profile)
 macro(add_test_pl_tests cmdline)
     get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME)
     message(STATUS "Adding tests in directory: ${TEST_DIR_NAME}")
-    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -C CORE)
-    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH)
-    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE)
-    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG)
+    add_test_pl_profile("${TEST_DIR_NAME}" ${cmdline} -C CORE)
+    add_test_pl_profile("${TEST_DIR_NAME}" ${cmdline} -T THOROUGH)
+    add_test_pl_profile("${TEST_DIR_NAME}" ${cmdline} -F FUTURE)
+    add_test_pl_profile("${TEST_DIR_NAME}" ${cmdline} -K KNOWNBUG)
 endmacro(add_test_pl_tests)
 
 add_subdirectory(ansi-c)

regression/cbmc/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc>"
+    $<TARGET_FILE:cbmc> -X smt-backend
 )

regression/cbmc/Makefile

@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -p -c ../../../src/cbmc/cbmc
+	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
 
 tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/cbmc/cbmc
+	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
 
 show:
 	@for dir in *; do \

regression/cbmc/integer-assignments1/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  __CPROVER_integer a, b;
+  a=0;
+  b=a;
+  b++;
+  b*=100;
+  __CPROVER_assert(0, "");
+}

regression/cbmc/integer-assignments1/test.desc

@@ -0,0 +1,7 @@
+CORE smt-backend
+main.c
+--trace --smt2
+^EXIT=10$
+^SIGNAL=0$
+^  b=100
+--

src/solvers/smt2/smt2_conv.cpp

@@ -1829,7 +1829,8 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
        src_type.id()==ID_unsignedbv ||
        src_type.id()==ID_c_bool ||
        src_type.id()==ID_fixedbv ||
-       src_type.id()==ID_pointer)
+       src_type.id()==ID_pointer ||
+       src_type.id()==ID_integer)
     {
       out << "(not (= ";
       convert_expr(src);
@@ -2274,6 +2275,17 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
     else
       UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float");
   }
+  else if(dest_type.id()==ID_integer)
+  {
+    if(src_type.id()==ID_bool)
+    {
+      out << "(ite ";
+      convert_expr(src);
+      out <<" 1 0)";
+    }
+    else
+      UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> integer");
+  }
   else if(dest_type.id()==ID_c_bit_field)
   {
     std::size_t from_width=boolbv_width(src_type);
@@ -2917,7 +2929,7 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
 
         mp_integer element_size=
           pointer_offset_size(expr.type().subtype(), ns);
-        assert(element_size>0);
+        CHECK_RETURN(element_size>0);
 
         out << "(bvadd ";
         convert_expr(p);
@@ -3084,7 +3096,15 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
 {
   assert(expr.operands().size()==2);
 
-  if(expr.type().id()==ID_unsignedbv ||
+  if(expr.type().id()==ID_integer)
+  {
+    out << "(- ";
+    convert_expr(expr.op0());
+    out << " ";
+    convert_expr(expr.op1());
+    out << ")";
+  }
+  else if(expr.type().id()==ID_unsignedbv ||
      expr.type().id()==ID_signedbv ||
      expr.type().id()==ID_fixedbv)
   {