Merge pull request diffblue#4519 from tautschnig/float-byte-extract

Use bv_typet to fix type consistency in byte-operator lowering
smowton · Apr 12, 2019 · 05769c0 · 05769c0
2 parents eed359b + ee07f0a
commit 05769c0
Show file tree

Hide file tree

Showing 16 changed files with 158 additions and 106 deletions.
diff --git a/regression/cbmc/Bitfields3/paths.desc b/regression/cbmc/Bitfields3/paths.desc
@@ -6,3 +6,6 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test is marked broken-smt-backend for performance reasons only: it passes,
+but takes 5 seconds to do so.
diff --git a/regression/cbmc/Bitfields3/test.desc b/regression/cbmc/Bitfields3/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=10$

diff --git a/regression/cbmc/Pointer_Arithmetic11/test.desc b/regression/cbmc/Pointer_Arithmetic11/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check --little-endian
 ^EXIT=0$

diff --git a/regression/cbmc/Pointer_byte_extract2/test.desc b/regression/cbmc/Pointer_byte_extract2/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=10$

diff --git a/regression/cbmc/Pointer_byte_extract9/test.desc b/regression/cbmc/Pointer_byte_extract9/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=10$

diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^\*\* Results:$

diff --git a/regression/cbmc/byte_update3/test.desc b/regression/cbmc/byte_update3/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$

diff --git a/regression/cbmc/byte_update5/test.desc b/regression/cbmc/byte_update5/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$

diff --git a/regression/cbmc/memory_allocation2/test.desc b/regression/cbmc/memory_allocation2/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --bounds-check
 ^EXIT=10$

diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp
@@ -260,7 +260,7 @@ bool boolbvt::type_conversion(
     {
       INVARIANT(
         src_width == dest_width,
-        "source bitvector with shall equal the destination bitvector width");
+        "source bitvector width shall equal the destination bitvector width");
       dest=src;
       return false;
     }
@@ -415,24 +415,31 @@ bool boolbvt::type_conversion(
       }
       break;
 
-    default:
-      if(src_type.id()==ID_bool)
-      {
-        // bool to integer
-
+      case bvtypet::IS_BV:
         INVARIANT(
-          src_width == 1, "bitvector of type boolean shall have width one");
+          src_width == dest_width,
+          "source bitvector width shall equal the destination bitvector width");
+        dest = src;
+        return false;
 
-        for(std::size_t i=0; i<dest_width; i++)
+      default:
+        if(src_type.id() == ID_bool)
         {
-          if(i==0)
-            dest.push_back(src[0]);
-          else
-            dest.push_back(const_literal(false));
-        }
+          // bool to integer
 
-        return false;
-      }
+          INVARIANT(
+            src_width == 1, "bitvector of type boolean shall have width one");
+
+          for(std::size_t i = 0; i < dest_width; i++)
+          {
+            if(i == 0)
+              dest.push_back(src[0]);
+            else
+              dest.push_back(const_literal(false));
+          }
+
+          return false;
+        }
     }
     break;