Refactored the wrapping of the entry point functionality into its own file, and added support for goto-analyzer

Author: NlightNFotis

src/ansi-c/ansi_c_entry_point.cpp

@@ -22,6 +22,7 @@ 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"
@@ -478,16 +479,3 @@ bool ansi_c_entry_point(
 
   return false;
 }
-
-// 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;
-}

src/ansi-c/ansi_c_entry_point.h

@@ -12,15 +12,11 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/symbol_table.h>
 #include <util/message.h>
-#include <util/std_code.h>
 
 bool ansi_c_entry_point(
   symbol_tablet &symbol_table,
   const std::string &standard_main,
   message_handlert &message_handler,
   bool wrap_entry_point);
 
-code_whilet wrap_entry_point_in_while(
-  code_function_callt &call_main);
-
 #endif // CPROVER_ANSI_C_ANSI_C_ENTRY_POINT_H

src/cbmc/cbmc_parse_options.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/parse_options.h>
 
 #include <langapi/language_ui.h>
+#include <langapi/wrap_entry_point.h>
 
 #include <analyses/goto_check.h>
 
@@ -63,7 +64,7 @@ class optionst;
   "(java-cp-include-files):" \
   "(localize-faults)(localize-faults-method):" \
   "(lazy-methods)" \
-  "(wrap-entry-point-in-while)" \
+  WRAP_ENTRY_POINT_IN_WHILE_TRUE \
   "(test-invariant-failure)" \
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -108,6 +108,7 @@ graphs in DOT format.
 #include <util/parse_options.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>
@@ -149,6 +150,7 @@ class optionst;
   "(unwind-bounds)" \
   "(unwind-bounds-threshold):" \
   "(unwindset)" \
+  WRAP_ENTRY_POINT_IN_WHILE_TRUE \
   "(functions-ignore)" \
   "(functions-full)"
 

src/langapi/Makefile

@@ -2,6 +2,7 @@ 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

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: Wrap the designated entry point into a while(true) loop.
+
+Author: Diffblue Limited (c) 2017
+
+Date: August 2017
+
+\*******************************************************************/
+
+/// \file
+/// Wrap the designated entry point into a while(true) loop.
+
+#include "wrap_entry_point.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;
+}

src/langapi/wrap_entry_point.h

@@ -0,0 +1,22 @@
+/*******************************************************************\
+
+Module: Wrap the designated entry point into a while(true) loop.
+
+Author: Diffblue Limited (c) 2017
+
+Date: August 2017
+
+\*******************************************************************/
+
+#ifndef WRAP_ENTRY_POINT_H
+#define WRAP_ENTRY_POINT_H
+
+#include <util/std_code.h>
+
+/// Command line option (to be shared by the different tools)
+#define WRAP_ENTRY_POINT_IN_WHILE_TRUE "(wrap-entry-point-in-while)"
+
+code_whilet wrap_entry_point_in_while(
+  code_function_callt &call_main);
+
+#endif // WRAP_ENTRY_POINT_H