Implemented all the changes asked for by Martin

Author: NlightNFotis

src/ansi-c/ansi_c_entry_point.cpp

@@ -22,13 +22,25 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/string_constant.h>
 
 #include <goto-programs/goto_functions.h>
-#include <langapi/wrap_entry_point.h>
 #include <linking/static_lifetime_init.h>
 
 #include "ansi_c_entry_point.h"
 #include "ansi_c_language.h"
 #include "c_nondet_symbol_factory.h"
 
+// Build and return a while(true) statement nesting the function call
+// passed as a parameter.
+code_whilet wrap_entry_point_in_while(code_function_callt &call_main)
+{
+  exprt true_expr;
+  code_whilet while_expr;
+  true_expr.make_true();
+  while_expr.cond()=true_expr;
+  while_expr.body()=call_main;
+
+  return while_expr;
+}
+
 exprt::operandst build_function_environment(
   const code_typet::parameterst &parameters,
   code_blockt &init_code,
@@ -123,8 +135,7 @@ void record_function_outputs(
 bool ansi_c_entry_point(
   symbol_tablet &symbol_table,
   const std::string &standard_main,
-  message_handlert &message_handler,
-  bool wrap_entry_point)
+  message_handlert &message_handler)
 {
   // check if entry point is already there
   if(symbol_table.symbols.find(goto_functionst::entry_point())!=

src/ansi-c/ansi_c_entry_point.h

@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
 bool ansi_c_entry_point(
   symbol_tablet &symbol_table,
   const std::string &standard_main,
-  message_handlert &message_handler,
-  bool wrap_entry_point);
+  message_handlert &message_handler);
 
 #endif // CPROVER_ANSI_C_ANSI_C_ENTRY_POINT_H

src/ansi-c/ansi_c_language.cpp

@@ -127,8 +127,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(),
-     config.ansi_c.wrap_entry_point_in_while))
+  if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
   {
     return true;
   }

src/cbmc/cbmc_parse_options.h

@@ -14,9 +14,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/ui_message.h>
 #include <util/parse_options.h>
+#include <util/config.h>
 
 #include <langapi/language_ui.h>
-#include <langapi/wrap_entry_point.h>
 
 #include <analyses/goto_check.h>
 

src/cpp/cpp_language.cpp

@@ -135,8 +135,7 @@ bool cpp_languaget::typecheck(
 
 bool cpp_languaget::final(symbol_tablet &symbol_table)
 {
-  if(ansi_c_entry_point(symbol_table, "main", get_message_handler(),
-     config.ansi_c.wrap_entry_point_in_while))
+  if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
   {
     return true;
   }

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -106,10 +106,9 @@ graphs in DOT format.
 
 #include <util/ui_message.h>
 #include <util/parse_options.h>
+#include <util/config.h>
 
 #include <langapi/language_ui.h>
-#include <langapi/wrap_entry_point.h>
-
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
 

src/goto-cc/compile.cpp

@@ -368,7 +368,7 @@ bool compilet::link()
     symbol_table.remove(goto_functionst::entry_point());
     compiled_functions.function_map.erase(goto_functionst::entry_point());
 
-    if(ansi_c_entry_point(symbol_table, "main", get_message_handler(), false))
+    if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
       return true;
 
     // entry_point may (should) add some more functions.

src/langapi/Makefile

@@ -2,7 +2,6 @@ SRC = language_ui.cpp \
       language_util.cpp \
       languages.cpp \
       mode.cpp \
-      wrap_entry_point.cpp \
       # Empty last line
 INCLUDES= -I ..
 

src/langapi/wrap_entry_point.cpp

@@ -18,8 +18,6 @@ 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()

src/langapi/wrap_entry_point.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <list>
 
+#include <util/std_code.h>
+
 #include "ieee_float.h"
 #include "irep.h"
 
@@ -161,4 +163,15 @@ class configt
 
 extern configt config;
 
+/// 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_TRUE_STRING ")"
+
+/// Command line help text
+#define HELP_WRAP_ENTRY_POINT_IN_WHILE_TRUE \
+  " --wrap-entry-point-in-while  wrap the designated entry point function in a while(true) statement\n" // NOLINT(*)
+
 #endif // CPROVER_UTIL_CONFIG_H