Restructured the test generation code

src/cbmc/bmc_cover.cpp

@@ -21,7 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/xml_goto_trace.h>
 #include <goto-programs/json_goto_trace.h>
 
-#include <test-c-gen/c_test_case_generator.h>
+#include <test-c-gen/c_simple_test_case_generator.h>
 
 #include "bmc.h"
 #include "bv_cbmc.h"
@@ -106,14 +106,6 @@ class bmc_covert:
       return disjunction(tmp);
     }
   };
-
-  struct testt
-  {
-    goto_tracet goto_trace;
-    std::vector<irep_idt> covered_goals;
-    std::string source_code;
-    std::string test_function_name;
-  };
 
   inline irep_idt id(goto_programt::const_targett loc)
   {
@@ -315,10 +307,10 @@ bool bmc_covert::operator()()
 
   if (bmc.options.get_bool_option("gen-c-test-case"))
   {
+
     size_t test_case_no=0;
     for(auto& test : tests)
     {
-      c_test_case_generatort gen(get_message_handler());
       std::vector<std::string> goal_names;
       for(const auto& goalid : test.covered_goals)
       {
@@ -328,14 +320,13 @@ bool bmc_covert::operator()()
           +id2string(goal_map.at(goalid).source_location.get_line()));
       }
 
-      // Compute the test function name
-      test.test_function_name=gen.get_test_function_name(bmc.ns.get_symbol_table(),
-                                                          goto_functions, test_case_no);
+      c_simple_test_case_generatort gen(get_message_handler(), bmc.options,
+        bmc.ns.get_symbol_table(), goto_functions, test, test_case_no, true);
 
-      // Compute the test code
-      test.source_code=gen.generate_tests(bmc.options,bmc.ns.get_symbol_table(),
-                                                   goto_functions,test.goto_trace,
-                                                   test_case_no,goal_names);
+      // Generate a full file for this test
+      gen();
+      test.test_function_name=gen.get_test_function_name(test_case_no);
+      test.source_code=gen.get_test_body();
 
       ++test_case_no;
     }
@@ -364,6 +355,7 @@ bool bmc_covert::operator()()
 
       for(const auto& it : tests)
       {
+        status() << it.test_function_name << ":" << eom;
         if(it.source_code.length()!=0)
           status() << it.source_code << '\n';
       }

src/test-c-gen/Makefile

@@ -1,4 +1,5 @@
-SRC = c_test_case_generator.cpp expr2cleanc.cpp function_parameter_builder.cpp function_return_builder.cpp c_test_file.cpp
+SRC = c_test_case_generator.cpp expr2cleanc.cpp function_parameter_builder.cpp \
+      function_return_builder.cpp c_test_file.cpp c_simple_test_case_generator.cpp
 
 INCLUDES= -I ..
 

src/test-c-gen/c_simple_test_case_generator.cpp

@@ -0,0 +1,111 @@
+/*******************************************************************\
+
+ Module: C Test Case Generator
+
+ Author: Thomas Kiley, [email protected]
+
+\*******************************************************************/
+
+#include <test-c-gen/c_simple_test_case_generator.h>
+#include <test-c-gen/c_test_file.h>
+#include <test-c-gen/expr2cleanc.h>
+#include <string>
+#include <vector>
+
+c_simple_test_case_generatort::c_simple_test_case_generatort(
+  message_handlert &_message_handler,
+  const optionst &options,
+  const symbol_tablet &symbol_table,
+  const goto_functionst &goto_functions,
+  const testt &test,
+  size_t test_index,
+  bool using_test_main)
+  : c_test_case_generatort(_message_handler, options, symbol_table,
+      goto_functions, test, test_index),
+      using_test_main(using_test_main)
+{
+}
+
+/*******************************************************************\
+Function: c_simple_test_case_generatort::add_includes
+Inputs:
+ test_file - The C file to add the includes to
+Purpose: To add the includes required for a simple test harness
+\*******************************************************************/
+void c_simple_test_case_generatort::add_includes(c_test_filet &test_file)
+{
+  test_file.add_line_at_root_indentation("#include <assert.h>");
+  test_file.add_line_at_root_indentation("#include <stdio.h>");
+
+  // We only require stdlib if we are making a main method that isn't called
+  // main (in this case we need to call things like exit(0) when the function
+  // is done.
+  if(using_test_main)
+  {
+    test_file.add_line_at_root_indentation("#include <stdlib.h>");
+  }
+  test_file.add_empty_line();
+
+  // Add the include for the file after the initial includes
+  c_test_case_generatort::add_includes(test_file);
+}
+
+/*******************************************************************\
+Function: c_simple_test_case_generatort::add_main_method
+Inputs:
+ test_file - The C file to add the includes to
+ tests - The tests that need to be called
+Purpose: To create the main method that will call all the tests
+         included inside this file
+\*******************************************************************/
+void c_simple_test_case_generatort::add_main_method(c_test_filet &test_file,
+  const testt &test)
+{
+  // Create main method
+  const std::string main_method_name=using_test_main?"test_main":"main";
+
+  test_file.add_function("int", main_method_name,
+    {{"int", "argc"}, {"char*", "argv"}});
+
+  std::ostringstream test_function_call_builder;
+  test_function_call_builder << test.test_function_name;
+  test_function_call_builder << "();";
+  test_file.add_line_at_current_indentation(test_function_call_builder.str());
+
+  test_file.add_empty_line();
+
+  // Shutdown the application correctly
+  if(using_test_main)
+  {
+    test_file.add_line_at_current_indentation("exit(0);");
+  }
+
+  test_file.add_line_at_current_indentation("return 0;");
+  test_file.end_function();
+}
+
+/*******************************************************************\
+Function: c_simple_test_case_generatort::add_simple_assert
+Inputs:
+ test_file - The C test file being created
+ correct_expression - The expression representing the value expected
+ return_value_var - The name of the variable (including relevant nesting)
+Purpose: Add an assertion for a simple expression
+ \*******************************************************************/
+void c_simple_test_case_generatort::add_simple_assert(c_test_filet &test_file,
+  const exprt &correct_expression,
+  std::string return_value_var)
+{
+  std::ostringstream assert_builder;
+
+  assert_builder << "assert(";
+  assert_builder << return_value_var;
+  assert_builder << " == ";
+
+  std::string expected_return_value=e2c->convert(correct_expression);
+
+  assert_builder << expected_return_value;
+  assert_builder << ");";
+
+  test_file.add_line_at_current_indentation(assert_builder.str());
+}

src/test-c-gen/c_simple_test_case_generator.h

@@ -0,0 +1,40 @@
+/*******************************************************************\
+
+ Module: C Test Case Generator
+
+ Author: Thomas Kiley, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_TEST_C_GEN_C_SIMPLE_TEST_CASE_GENERATOR_H
+#define CPROVER_TEST_C_GEN_C_SIMPLE_TEST_CASE_GENERATOR_H
+
+#include <test-c-gen/c_test_case_generator.h>
+#include <string>
+#include <vector>
+
+class c_simple_test_case_generatort : public c_test_case_generatort
+{
+public:
+  c_simple_test_case_generatort(message_handlert &_message_handler,
+    const class optionst &options,
+    const class symbol_tablet &symbol_table,
+    const class goto_functionst &goto_functions,
+    const testt &test,
+    size_t test_index,
+    bool using_test_main);
+
+protected:
+  virtual void add_includes(class c_test_filet &test_file) override;
+  virtual void add_main_method(c_test_filet &test_file,
+    const testt &test) override;
+
+  virtual void add_simple_assert(class c_test_filet &test_file,
+    const exprt &correct_expression,
+    std::string ret_value_var);
+
+private:
+  bool using_test_main;
+};
+
+#endif // CPROVER_TEST_C_GEN_C_SIMPLE_TEST_CASE_GENERATOR_H