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

tautschnig · web-flow · commit 05769c02ab79 · 2019-04-12T06:52:14.000+01:00
Use bv_typet to fix type consistency in byte-operator lowering
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;
 
diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/solvers/lowering/byte_operators.cpp

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE broken-smt-backend`
	`1`	`+CORE`
`2`	`2`	`main.c`
`3`	`3`	`--pointer-check --bounds-check`
`4`	`4`	`^EXIT=0$`