C++ regression test fixes and whitespace changes (subset of #1260)

appveyor.yml

@@ -90,6 +90,9 @@ test_script:
     rmdir /s /q cpp\Decltype1
     rmdir /s /q cpp\Decltype2
     rmdir /s /q cpp\Function_Overloading1
+    rmdir /s /q cpp\Resolver10
+    rmdir /s /q cpp\Resolver11
+    rmdir /s /q cpp\Template_Parameters1
     rmdir /s /q cpp\enum2
     rmdir /s /q cpp\enum7
     rmdir /s /q cpp\enum8

regression/CMakeLists.txt

@@ -30,6 +30,7 @@ add_subdirectory(goto-instrument)
 add_subdirectory(cpp)
 add_subdirectory(cbmc-cover)
 add_subdirectory(goto-instrument-typedef)
+add_subdirectory(smt2_solver)
 add_subdirectory(strings)
 add_subdirectory(invariants)
 add_subdirectory(goto-diff)
@@ -41,4 +42,4 @@ endif()
 add_subdirectory(goto-cc-cbmc)
 add_subdirectory(cbmc-cpp)
 add_subdirectory(goto-cc-goto-analyzer)
-
+add_subdirectory(systemc)

regression/Makefile

@@ -18,6 +18,7 @@ DIRS = cbmc \
        goto-cc-cbmc \
        cbmc-cpp \
        goto-cc-goto-analyzer \
+       systemc
        # Empty last line
 
 # Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks

regression/cbmc/cpp1/main.cpp

@@ -0,0 +1,48 @@
+#include <cassert>
+
+template <class T>
+class sc_signal
+{
+public:
+    T data;
+    sc_signal(){}
+    sc_signal(const char *p) {}
+    T read() {return data;}
+    void write(const T &d) {data = d;}
+};
+
+
+struct rbm
+{
+
+   sc_signal<unsigned int>  data_out;   //<L1>
+
+   sc_signal<bool>   done;  // <L2>
+
+   sc_signal<bool> conf_done;
+
+   void config();
+
+   rbm()
+   {
+
+   }
+
+};
+
+
+void rbm::config()
+{
+   do {
+         conf_done.write(true);
+         assert(conf_done.data==true);
+    } while ( !conf_done.read() );
+}
+
+int main()
+{
+    rbm IMPL;
+    IMPL.config();
+
+    return 0;
+}

regression/cbmc/cpp1/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This has been reported as #661.

regression/cbmc/cpp2/main.cpp

@@ -0,0 +1,47 @@
+#include <cassert>
+#include <stdint.h>
+#include <stdbool.h>
+
+#undef HOTFIX
+
+typedef struct {
+  uint32_t value_31_0 : 32;
+} signal32_t;
+
+typedef struct {
+  uint8_t value_0_0 : 1;
+} signal1_t;
+
+static inline bool yosys_simplec_get_bit_25_of_32(const signal32_t *sig)
+{
+  return (sig->value_31_0 >> 25) & 1;
+}
+
+struct rvfi_insn_srai_state_t
+{
+  signal32_t rvfi_insn;
+  signal32_t rvfi_rs1_rdata;
+  signal1_t _abc_1398_n364;
+  signal1_t _abc_1398_n363;
+};
+
+void test(rvfi_insn_srai_state_t state, bool valid)
+{
+#ifndef HOTFIX
+  state._abc_1398_n364.value_0_0 = yosys_simplec_get_bit_25_of_32(&state.rvfi_insn) ?
+      yosys_simplec_get_bit_25_of_32(&state.rvfi_rs1_rdata) : state._abc_1398_n363.value_0_0;
+#else
+  state._abc_1398_n364.value_0_0 = yosys_simplec_get_bit_25_of_32(&state.rvfi_insn) ?
+      yosys_simplec_get_bit_25_of_32(&state.rvfi_rs1_rdata) : (bool)state._abc_1398_n363.value_0_0;
+#endif
+
+  assert(valid);
+}
+
+int main(int argc, char* argv[])
+{
+	rvfi_insn_srai_state_t state;
+  bool valid;
+  test(state, valid);
+  return 0;
+}

regression/cbmc/cpp2/test.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^equality without matching types
+--
+This has been reported as #933.

regression/cpp/Apple_extensions1/main.cpp

@@ -5,3 +5,7 @@ void * _Nonnull p2;
 // block pointer
 void (^p3)(void);
 #endif
+
+int main(int argc, char* argv[])
+{
+}

regression/cpp/Apple_extensions1/test.desc

@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.cpp
 
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 ^CONVERSION ERROR$
+--
+This is being tracked in #1647.

regression/cpp/Constant2/main.cpp

@@ -1,3 +1,5 @@
+#include <cassert>
+
 int const C=10;
 
 int main()

regression/cpp/List_initialization1/main.cpp

@@ -26,7 +26,7 @@ int main()
   int y { 1 };
   x={ 1 };
   x=int { 1 };
-  x=(int) { 1 }
+  x=(int) { 1 };
   p=new int { 1 };
   some_function({1});
 }

regression/cpp/ModeC1/main.cpp

@@ -1,5 +1,6 @@
 int cpp_f(int fkt_argument)
 {
+  return 0;
 }
 
 extern "C" void f(int fkt_argument)
@@ -27,4 +28,6 @@ int main()
   f(0);
   g(0);
   g(0L);
+
+  return 0;
 }

regression/cpp/Qualifiers_In_Template_Specialisation1/main.cpp

@@ -1,5 +1,6 @@
 template <class T>
 class c {
+public:
   void fun (const T &arg);
 };
 
@@ -9,7 +10,7 @@ void c<long int>::fun (const long int &arg) { return; }
 int main(void) {
   c<long int> cl;
 
-  cl.fun();
+  cl.fun(0);
 
   return 0;
 }

regression/cpp/Resolver10/main.cpp

@@ -1,3 +1,5 @@
+#include <cassert>
+
 struct A
 {
   int i;
@@ -10,7 +12,7 @@ struct B: A
   {
     i = 1;
     A();
-    assert(i==1);
+    __CPROVER_assert(i==1, "");
   }
 };
 

regression/cpp/Resolver11/main.cpp

@@ -1,3 +1,5 @@
+#include <cassert>
+
 struct A
 {
   bool func() { return false; }
@@ -17,7 +19,7 @@ struct A
 int main()
 {
   A a;
-  assert(a.test()==false);
+  __CPROVER_assert(a.test() == false, "");
   const A a2;
-  assert(a2.test()==true);
+  __CPROVER_assert(a2.test() == true, "");
 }

regression/cpp/Template_Instantiation2/main.cpp

@@ -6,3 +6,8 @@ public :
 
 template<>
 int c<char>::f00(const char*);
+
+int main(int argc, char* argv[])
+{
+  return 0;
+}

regression/cpp/Template_Parameters1/main.ii → regression/cpp/Template_Parameters1/main.cpp

@@ -1,3 +1,5 @@
+#include <cassert>
+
 // V depends on Ty
 template<typename Ty, Ty V>
 class T
@@ -10,6 +12,6 @@ T<int, 10> some_T;
 
 int main()
 {
-  assert(some_T.value==10);
+  __CPROVER_assert(some_T.value == 10, "");
 }
 

regression/cpp/Template_Parameters1/test.desc

@@ -1,5 +1,5 @@
 CORE
-main.ii
+main.cpp
 
 ^EXIT=0$
 ^SIGNAL=0$

regression/cpp/Template_Specialisation2/main.ii

@@ -15,3 +15,6 @@ struct __member_pointer_traits_imp<_Rp (_Class::*)() const>
 {
 };
 
+int main(int argc, char* argv[])
+{
+}

regression/cpp/Trailing_Return_Type1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.cpp
-
+-std=c++11
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cpp/auto1/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.cpp
-
+-std=c++11
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cpp/enum8/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.cpp
---std=c++11
+-std=c++11
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cpp/sizeof2/main.cpp

@@ -5,9 +5,12 @@ template <class T>
 int size()
 {
   sizeof(T);
+  return 0;
 }
 
 int main()
 {
   size<int>();
+
+  return 0;
 }

regression/cpp/type_traits_essentials1/main.cpp

@@ -55,6 +55,6 @@ class X
 
 int main(int argc, char* argv[])
 {
-  X<> x;
+  X<true> x;
   return x.val()?0:1;
 }

regression/cpp/type_traits_essentials1/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.cpp
-
+-std=c++11
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cpp/typecast_ambiguity2/main.cpp

@@ -5,6 +5,7 @@ int foo(int)
 
 unsigned some_function(void)
 {
+  return 0;
 }
 
 int main()

regression/cpp/virtual1/main.cpp

@@ -1,4 +1,6 @@
-#include <stdio.h>
+#include <cassert>
+#include <cstdio>
+
 class base
 {
 public:
@@ -26,7 +28,7 @@ int main (void)
     base* D = new derived;
     int a = D->func();
     delete D;
-    __CPROVER_assert(a == 2, "Property 1");
+    assert(a == 2);
     return a;
 }
 

regression/smt2_solver/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:smt2_solver>"
+)