esbmc · lucasccordeiro · Feb 21, 2024 · Feb 20, 2024 · Feb 20, 2024
diff --git a/regression/esbmc-cpp/cpp/ch2_5/test.desc b/regression/esbmc-cpp/cpp/ch2_5/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 --unwind 10 --no-unwinding-assertions --timeout 900
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/esbmc-cpp/cpp/cpp_stack_top_bug/test.desc b/regression/esbmc-cpp/cpp/cpp_stack_top_bug/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 --k-induction-parallel 
 ^VERIFICATION FAILED$
diff --git a/regression/esbmc-cpp/cpp/llbmc_stack-test/test.desc b/regression/esbmc-cpp/cpp/llbmc_stack-test/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 --unwind 2 --no-unwinding-assertions --timeout 900
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/esbmc-cpp/deque/deque_empty/test.desc b/regression/esbmc-cpp/deque/deque_empty/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 --unwind 10 --no-unwinding-assertions --timeout 900
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/esbmc-cpp/deque/deque_empty_bug/test.desc b/regression/esbmc-cpp/deque/deque_empty_bug/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 --unwind 11 --no-unwinding-assertions --timeout 900
 ^VERIFICATION FAILED$
diff --git a/regression/esbmc-cpp/stack/stack_empty_bug/test.desc b/regression/esbmc-cpp/stack/stack_empty_bug/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 --unwind 15 --no-unwinding-assertions --timeout 900
 ^VERIFICATION FAILED$
diff --git a/regression/esbmc-cpp/stack/stack_pop/test.desc b/regression/esbmc-cpp/stack/stack_pop/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 --unwind 10 --no-unwinding-assertions --timeout 900
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/esbmc-cpp/stack/stack_pop_bug/test.desc b/regression/esbmc-cpp/stack/stack_pop_bug/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 --unwind 10 --no-unwinding-assertions --timeout 900
 ^VERIFICATION FAILED$
diff --git a/regression/esbmc-cpp/stack/stack_push_bug/test.desc b/regression/esbmc-cpp/stack/stack_push_bug/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 --unwind 10 --no-unwinding-assertions --timeout 900
 ^VERIFICATION FAILED$
diff --git a/regression/esbmc-cpp/vector/ch11_16/test.desc b/regression/esbmc-cpp/vector/ch11_16/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 --unwind 10 --no-unwinding-assertions --timeout 900
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/esbmc-cpp/vector/ch11_24/test.desc b/regression/esbmc-cpp/vector/ch11_24/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 --unwind 10 --no-unwinding-assertions --timeout 900
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/esbmc-cpp/vector/ch21_10/test.desc b/regression/esbmc-cpp/vector/ch21_10/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 --unwind 10 --no-unwinding-assertions --timeout 900
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/esbmc-cpp/vector/vector30/test.desc b/regression/esbmc-cpp/vector/vector30/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 --unwind 15 --no-unwinding-assertions --timeout 900
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/esbmc-cpp/vector/vector50/test.desc b/regression/esbmc-cpp/vector/vector50/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.cpp
 --unwind 15 --no-unwinding-assertions --timeout 900
 ^VERIFICATION FAILED$
diff --git a/regression/k-induction/cpp_stack_top_bug/test.desc b/regression/k-induction/cpp_stack_top_bug/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+THOROUGH
 main.cpp
 --k-induction 
 ^VERIFICATION FAILED$
diff --git a/src/clang-c-frontend/clang_c_adjust.h b/src/clang-c-frontend/clang_c_adjust.h
@@ -63,6 +63,7 @@ class clang_c_adjust
   adjust_function_call_arguments(side_effect_expr_function_callt &expr);
   void do_special_functions(side_effect_expr_function_callt &expr);
   void adjust_operands(exprt &expr);
+  virtual void adjust_if(exprt &expr);
 
   /**
    * methods for code (codet) adjustment

diff --git a/src/clang-c-frontend/clang_c_adjust_expr.cpp b/src/clang-c-frontend/clang_c_adjust_expr.cpp
@@ -123,14 +123,7 @@ void clang_c_adjust::adjust_expr(exprt &expr)
   }
   else if (expr.id() == "if")
   {
-    // Check all operands
-    adjust_operands(expr);
-
-    // If the condition is not of boolean type, it must be casted
-    gen_typecast(ns, expr.op0(), bool_type());
-
-    // Typecast both the true and false results
-    gen_typecast_arithmetic(ns, expr.op1(), expr.op2());
+    adjust_if(expr);
   }
   else if (expr.id() == "builtin_va_arg")
   {
@@ -1332,6 +1325,19 @@ void clang_c_adjust::adjust_operands(exprt &expr)
     adjust_expr(op);
 }
 
+void clang_c_adjust::adjust_if(exprt &expr)
+{
+  // Check all operands
+  adjust_operands(expr);
+
+  // If the condition is not of boolean type, it must be casted
+  gen_typecast(ns, expr.op0(), bool_type());
+
+  // Typecast both the true and false results
+  // If the types are inconsistent
+  gen_typecast_arithmetic(ns, expr.op1(), expr.op2());
+}
+
 void clang_c_adjust::align_se_function_call_return_type(
   exprt &,
   side_effect_expr_function_callt &)

diff --git a/src/clang-cpp-frontend/clang_cpp_adjust.h b/src/clang-cpp-frontend/clang_cpp_adjust.h
@@ -47,6 +47,7 @@ class clang_cpp_adjust : public clang_c_adjust
   void adjust_expr_rel(exprt &expr) override;
   void adjust_new(exprt &expr);
   void adjust_cpp_member(member_exprt &expr);
+  void adjust_if(exprt &expr) override;
 
   /**
    * methods for implicit GOTO code generation

diff --git a/src/clang-cpp-frontend/clang_cpp_adjust_expr.cpp b/src/clang-cpp-frontend/clang_cpp_adjust_expr.cpp
@@ -1,5 +1,7 @@
+#include <clang-c-frontend/typecast.h>
 #include <clang-cpp-frontend/clang_cpp_adjust.h>
 #include <util/c_sizeof.h>
+#include <util/c_types.h>
 #include <util/destructor.h>
 #include <util/expr_util.h>
 
@@ -130,6 +132,19 @@ void clang_cpp_adjust::adjust_cpp_member(member_exprt &expr)
   expr.swap(method_call);
 }
 
+void clang_cpp_adjust::adjust_if(exprt &expr)
+{
+  // Check all operands
+  adjust_operands(expr);
+
+  // If the condition is not of boolean type, it must be casted
+  gen_typecast(ns, expr.op0(), bool_type());
+
+  // Typecast both the true and false results
+  gen_typecast(ns, expr.op1(), expr.type());
+  gen_typecast(ns, expr.op2(), expr.type());
+}
+
 void clang_cpp_adjust::adjust_side_effect_assign(side_effect_exprt &expr)
 {
   // sideeffect assign got be representing a binary operator
@@ -289,4 +304,4 @@ void clang_cpp_adjust::align_se_function_call_return_type(
   const typet &return_type = (typet &)f_op.type().return_type();
   if (return_type.id() != "constructor")
     expr.type() = return_type;
-}
+}