Moved the command line argument handling, and removed the code specific to it in ansi-c and cpp folders. Also added a basic test for cbmc that passes for now.

Author: NlightNFotis

regression/cbmc/wrap_entry_point_in_while_true/main.c

@@ -1,4 +1,7 @@
-int main(int argc, char **argv)
+int g = 0;
+
+int main(void)
 {
-    return 0;
+    assert(g == 0);
+    g = (g == 0) ? 1 : 0;
 }

regression/cbmc/wrap_entry_point_in_while_true/test.desc

@@ -1,8 +1,10 @@
 CORE
 main.c
---show-goto-functions --wrap-entry-point-in-while
-^EXIT=0$
+--wrap-entry-point-in-while --unwind 100
+^EXIT=10$
 ^SIGNAL=0$
-^     1: main\(argc', argv'\);$
-^        GOTO 1$
+^\[main.assertion.1\] assertion g == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+^VERIFICATION SUCCESSFUL$
 --

src/ansi-c/ansi_c_entry_point.cpp

@@ -447,7 +447,7 @@ bool ansi_c_entry_point(
         message_handler);
   }
 
-  if(wrap_entry_point)
+  if(config.ansi_c.wrap_entry_point_in_while)
   {
     code_whilet wrapped_main=wrap_entry_point_in_while(call_main);
     init_code.move_to_operands(wrapped_main);

src/ansi-c/ansi_c_language.cpp

@@ -27,11 +27,6 @@ Author: Daniel Kroening, [email protected]
 #include "ansi_c_internal_additions.h"
 #include "type2name.h"
 
-void ansi_c_languaget::get_language_options(const cmdlinet &cmd)
-{
-  wrap_entry_point=cmd.isset("wrap-entry-point-in-while");
-}
-
 std::set<std::string> ansi_c_languaget::extensions() const
 {
   return { "c", "i" };
@@ -133,7 +128,7 @@ bool ansi_c_languaget::typecheck(
 bool ansi_c_languaget::final(symbol_tablet &symbol_table)
 {
   if(ansi_c_entry_point(symbol_table, "main", get_message_handler(),
-     wrap_entry_point_in_while()))
+     config.ansi_c.wrap_entry_point_in_while))
   {
     return true;
   }

src/ansi-c/ansi_c_language.h

@@ -22,9 +22,6 @@ Author: Daniel Kroening, [email protected]
 class ansi_c_languaget:public languaget
 {
 public:
-  virtual void get_language_options(
-    const cmdlinet &) override;
-
   bool preprocess(
     std::istream &instream,
     const std::string &path,
@@ -79,12 +76,6 @@ class ansi_c_languaget:public languaget
 protected:
   ansi_c_parse_treet parse_tree;
   std::string parse_path;
-
-  bool wrap_entry_point_in_while() const
-  { return wrap_entry_point; }
-
-private:
-  bool wrap_entry_point;
 };
 
 languaget *new_ansi_c_language();

src/cpp/cpp_language.cpp

@@ -29,11 +29,6 @@ Author: Daniel Kroening, [email protected]
 #include "cpp_typecheck.h"
 #include "cpp_type2name.h"
 
-void cpp_languaget::get_language_options(const cmdlinet &cmd)
-{
-  wrap_entry_point=cmd.isset("wrap-entry-point-in-while");
-}
-
 std::set<std::string> cpp_languaget::extensions() const
 {
   std::set<std::string> s;
@@ -141,7 +136,7 @@ bool cpp_languaget::typecheck(
 bool cpp_languaget::final(symbol_tablet &symbol_table)
 {
   if(ansi_c_entry_point(symbol_table, "main", get_message_handler(),
-     wrap_entry_point_in_while()))
+     config.ansi_c.wrap_entry_point_in_while))
   {
     return true;
   }

src/cpp/cpp_language.h

@@ -24,9 +24,6 @@ Author: Daniel Kroening, [email protected]
 class cpp_languaget:public languaget
 {
 public:
-  virtual void get_language_options(
-    const cmdlinet &cmd) override;
-
   bool preprocess(
     std::istream &instream,
     const std::string &path,
@@ -88,9 +85,6 @@ class cpp_languaget:public languaget
 
   void modules_provided(std::set<std::string> &modules) override;
 
-  bool wrap_entry_point_in_while() const
-  { return wrap_entry_point; }
-
 protected:
   cpp_parse_treet cpp_parse_tree;
   std::string parse_path;
@@ -101,9 +95,6 @@ class cpp_languaget:public languaget
   {
     return "main";
   }
-
-private:
-  bool wrap_entry_point;
 };
 
 languaget *new_cpp_language();

src/langapi/wrap_entry_point.h

@@ -13,6 +13,10 @@ Date: August 2017
 
 #include <util/std_code.h>
 
+/// Command line option (to be shared by the different tools)
+/// (This contains the actual string, needed in config.cpp)
+#define WRAP_ENTRY_POINT_IN_WHILE_TRUE_STRING "wrap-entry-point-in-while"
+
 /// Command line option (to be shared by the different tools)
 #define WRAP_ENTRY_POINT_IN_WHILE_TRUE "(wrap-entry-point-in-while)"
 

src/util/config.cpp

@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
 #include "std_expr.h"
 #include "cprover_prefix.h"
 
+#include "langapi/wrap_entry_point.h"
+
 configt config;
 
 void configt::ansi_ct::set_16()
@@ -757,6 +759,9 @@ bool configt::set(const cmdlinet &cmdline)
   if(cmdline.isset('I'))
     ansi_c.include_paths=cmdline.get_values('I');
 
+  ansi_c.wrap_entry_point_in_while=
+    cmdline.isset(WRAP_ENTRY_POINT_IN_WHILE_TRUE_STRING);
+
   if(cmdline.isset("classpath"))
   {
     // Specifying -classpath or -cp overrides any setting of the

src/util/config.h

@@ -44,6 +44,7 @@ class configt
     bool use_fixed_for_float;
     bool for_has_scope;
     bool single_precision_constant;
+    bool wrap_entry_point_in_while;
     enum class c_standardt { C89, C99, C11 } c_standard;
     static c_standardt default_c_standard();