Added new tests for CBMC, and made the tests for goto-analyser more robust.

Author: NlightNFotis

regression/cbmc/wrap_entry_point_in_while_true/main.c

@@ -0,0 +1,4 @@
+int main(int argc, char **argv)
+{
+    return 0;
+}

regression/cbmc/wrap_entry_point_in_while_true/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions --wrap-entry-point-in-while
+^EXIT=0$
+^SIGNAL=0$
+^     1: main\(argc', argv'\);$
+^        GOTO 1$
+--

regression/cbmc/wrap_entry_point_in_while_true_custom_entry_point/main.c

@@ -0,0 +1,4 @@
+int skipWhitespace()
+{
+    return 120;
+}

regression/cbmc/wrap_entry_point_in_while_true_custom_entry_point/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions --wrap-entry-point-in-while --function skipWhitespace
+^EXIT=0$
+^SIGNAL=0$
+^     1: skipWhitespace\(\);$
+^        GOTO 1$
+--

regression/goto-analyzer/wrap_entry_point_in_while_true/main.c

@@ -1,4 +1,4 @@
 int main(int argc, char **argv)
 {
     return 0;
-}
+}

regression/goto-analyzer/wrap_entry_point_in_while_true/test.desc

@@ -4,12 +4,6 @@ main.c
 ^EXIT=6$
 ^SIGNAL=0$
 ^     1: IF FALSE THEN GOTO 2$
-^        // 22 file main.c line 1$
 ^        main\(argc', argv'\);$
-^        // 23 file main.c line 1$
-^        return' = main#return_value;$
-^        // 24 file main.c line 1$
-^        dead main#return_value;$
-^        // 25 no location$
 ^        GOTO 1$
---
+--

regression/goto-analyzer/wrap_entry_point_in_while_true_custom_entry_point/main.c

@@ -1,4 +1,4 @@
 int skipWhitespace()
 {
     return 120;
-}
+}

regression/goto-analyzer/wrap_entry_point_in_while_true_custom_entry_point/test.desc

@@ -4,12 +4,6 @@ main.c
 ^EXIT=6$
 ^SIGNAL=0$
 ^     1: IF FALSE THEN GOTO 2$
-^        // 18 file main.c line 1
 ^        skipWhitespace\(\);$
-^        // 19 file main.c line 1$
-^        return' = skipWhitespace#return_value;$
-^        // 20 file main.c line 1$
-^        dead skipWhitespace#return_value;$
-^        // 21 no location$
 ^        GOTO 1$
---
+--

regression/goto-instrument/wrap_entry_point_in_while_true/main.c

@@ -0,0 +1,4 @@
+int main(int argc, char **argv)
+{
+    return 0;
+}

regression/goto-instrument/wrap_entry_point_in_while_true/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--show-goto-functions --wrap-entry-point-in-while
+^EXIT=0$
+^SIGNAL=0$
+^     1: main\(argc', argv'\);$
+^        GOTO 1$
+--
+--
+This is tracked by the JIRA issue TYT-4: https://diffblue.atlassian.net/projects/TYT/issues/TYT-4

regression/goto-instrument/wrap_entry_point_in_while_true_custom_entry_point/main.c

@@ -0,0 +1,4 @@
+int skipWhitespace()
+{
+    return 120;
+}

regression/goto-instrument/wrap_entry_point_in_while_true_custom_entry_point/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--show-goto-functions --wrap-entry-point-in-while --function skipWhitespace
+^EXIT=0$
+^SIGNAL=0$
+^     1: skipWhitespace\(\);$
+^        GOTO 1$
+--
+--
+This is tracked by the JIRA issue TYT-4: https://diffblue.atlassian.net/projects/TYT/issues/TYT-4

src/ansi-c/ansi_c_entry_point.cpp

@@ -447,10 +447,13 @@ bool ansi_c_entry_point(
         message_handler);
   }
 
-  if (wrap_entry_point) {
-    auto wrapped_main = wrap_entry_point_in_while(call_main);
+  if(wrap_entry_point)
+  {
+    code_whilet wrapped_main=wrap_entry_point_in_while(call_main);
     init_code.move_to_operands(wrapped_main);
-  } else {
+  }
+  else
+  {
     init_code.move_to_operands(call_main);
   }
 

src/ansi-c/ansi_c_language.cpp

@@ -29,10 +29,7 @@ Author: Daniel Kroening, [email protected]
 
 void ansi_c_languaget::get_language_options(const cmdlinet &cmd)
 {
-    if (cmd.isset("wrap-entry-point-in-while"))
-    {
-      wrap_entry_point = true;
-    }
+  wrap_entry_point=cmd.isset("wrap-entry-point-in-while");
 }
 
 std::set<std::string> ansi_c_languaget::extensions() const
@@ -136,8 +133,10 @@ 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()))
+     wrap_entry_point_in_while()))
+  {
     return true;
+  }
 
   return false;
 }
@@ -221,6 +220,7 @@ bool ansi_c_languaget::to_expr(
      expr.type().id()==ID_empty &&
      expr.operands().size()==1)
     expr=expr.op0();
+
   return result;
 }
 

src/ansi-c/ansi_c_language.h

@@ -70,9 +70,6 @@ class ansi_c_languaget:public languaget
   languaget *new_language() override
   { return new ansi_c_languaget; }
 
-  bool wrap_entry_point_in_while()
-  { return wrap_entry_point; }
-
   std::string id() const override { return "C"; }
   std::string description() const override { return "ANSI-C 99"; }
   std::set<std::string> extensions() const override;
@@ -83,6 +80,9 @@ class ansi_c_languaget:public languaget
   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;
 };

src/cbmc/cbmc_parse_options.cpp

@@ -65,8 +65,6 @@ Author: Daniel Kroening, [email protected]
 #include "version.h"
 #include "xml_interface.h"
 
-
-
 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv):
   parse_options_baset(CBMC_OPTIONS, argc, argv),
   xml_interfacet(cmdline),
@@ -185,9 +183,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
       cmdline.get_value("localize-faults-method"));
   }
 
-  if (cmdline.isset("wrap-entry-point-in-while"))
-    options.set_option("wrap-entry-point-in-while", true);
-
   if(cmdline.isset("unwind"))
     options.set_option("unwind", cmdline.get_value("unwind"));
 
@@ -604,6 +599,7 @@ int cbmc_parse_optionst::get_goto_program(
       }
 
       language->set_message_handler(get_message_handler());
+
       status() << "Parsing " << filename << eom;
 
       if(language->parse(infile, filename))

src/cpp/cpp_language.cpp

@@ -31,10 +31,7 @@ Author: Daniel Kroening, [email protected]
 
 void cpp_languaget::get_language_options(const cmdlinet &cmd)
 {
-    if (cmd.isset("wrap-entry-point-in-while"))
-    {
-      wrap_entry_point = true;
-    }
+  wrap_entry_point=cmd.isset("wrap-entry-point-in-while");
 }
 
 std::set<std::string> cpp_languaget::extensions() const
@@ -144,8 +141,10 @@ 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()))
+     wrap_entry_point_in_while()))
+  {
     return true;
+  }
 
   return false;
 }

src/cpp/cpp_language.h

@@ -88,7 +88,7 @@ class cpp_languaget:public languaget
 
   void modules_provided(std::set<std::string> &modules) override;
 
-  bool wrap_entry_point_in_while()
+  bool wrap_entry_point_in_while() const
   { return wrap_entry_point; }
 
 protected:

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1554,7 +1554,6 @@ 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,7 +16,6 @@ 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>
@@ -79,7 +78,6 @@ 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.cpp

@@ -20,8 +20,8 @@ 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;
+  while_expr.cond()=true_expr;
+  while_expr.body()=call_main;
 
   return while_expr;
 }

src/langapi/wrap_entry_point.h

@@ -8,8 +8,8 @@ Date: August 2017
 
 \*******************************************************************/
 
-#ifndef WRAP_ENTRY_POINT_H
-#define WRAP_ENTRY_POINT_H
+#ifndef CPROVER_LANGAPI_WRAP_ENTRY_POINT_H
+#define CPROVER_LANGAPI_WRAP_ENTRY_POINT_H
 
 #include <util/std_code.h>
 
@@ -23,4 +23,4 @@ Date: August 2017
 code_whilet wrap_entry_point_in_while(
   code_function_callt &call_main);
 
-#endif // WRAP_ENTRY_POINT_H
+#endif // CPROVER_LANGAPI_WRAP_ENTRY_POINT_H