Added the command line argument support for while(true) wrapping of the entry point to the goto-instrument tool, and added an associated help text to the other tools.

Author: NlightNFotis

src/cbmc/cbmc_parse_options.cpp

@@ -1023,6 +1023,7 @@ void cbmc_parse_optionst::help()
     " --round-to-minus-inf         rounding towards minus infinity\n"
     " --round-to-zero              rounding towards zero\n"
     " --function name              set main function name\n"
+    HELP_WRAP_ENTRY_POINT_IN_WHILE_TRUE
     "\n"
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -757,6 +757,7 @@ void goto_analyzer_parse_optionst::help()
     " --gcc                        use GCC as preprocessor\n"
     #endif
     " --no-library                 disable built-in abstract C library\n"
+    HELP_WRAP_ENTRY_POINT_IN_WHILE_TRUE
     "\n"
     "Java Bytecode frontend options:\n"
     " --classpath dir/jar          set the classpath\n"

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1554,6 +1554,7 @@ void goto_instrument_parse_optionst::help()
     " --log <file>                 log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
     " --remove-function-pointers   replace function pointers by case statement over function calls\n" // NOLINT(*)
     HELP_REMOVE_CONST_FUNCTION_POINTERS
+    HELP_WRAP_ENTRY_POINT_IN_WHILE_TRUE
     " --add-library                add models of C library functions\n"
     " --model-argc-argv <n>        model up to <n> command line arguments\n"
     // NOLINTNEXTLINE(whitespace/line_length)

src/goto-instrument/goto_instrument_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 <goto-programs/goto_functions.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/remove_const_function_pointers.h>
@@ -78,6 +79,7 @@ Author: Daniel Kroening, [email protected]
   "(show-threaded)(list-calls-args)(print-path-lengths)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):" \
+  WRAP_ENTRY_POINT_IN_WHILE_TRUE \
   "(remove-calls-nobody)"
 
 class goto_instrument_parse_optionst:

src/langapi/wrap_entry_point.h

@@ -16,6 +16,10 @@ Date: August 2017
 /// Command line option (to be shared by the different tools)
 #define WRAP_ENTRY_POINT_IN_WHILE_TRUE "(wrap-entry-point-in-while)"
 
+/// 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(*)
+
 code_whilet wrap_entry_point_in_while(
   code_function_callt &call_main);