Merge pull request #2291 from tautschnig/c++-fixes-1

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

Author: tautschnig

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()