Merge pull request #166 from diffblue/feature/wrap_entry_point_martin_changes

[TYT-5] Address Martin's comments of the Cyclic Dependency Analysis

Author: Thomas Kiley

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$
 --

regression/cbmc/wrap_entry_point_in_while_true_custom_entry_point/main.c

@@ -1,4 +1,7 @@
-int skipWhitespace()
+int g = 0;
+
+int skipWhitespace(void)
 {
-    return 120;
+    assert(g == 0);
+    g = (g == 0) ? 1 : 0;
 }

regression/cbmc/wrap_entry_point_in_while_true_custom_entry_point/test.desc

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

regression/goto-analyzer/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/goto-analyzer/wrap_entry_point_in_while_true/test.desc

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

regression/goto-analyzer/wrap_entry_point_in_while_true_custom_entry_point/main.c

@@ -1,4 +1,7 @@
-int skipWhitespace()
+int g = 0;
+
+int skipWhitespace(void)
 {
-    return 120;
+    assert(g == 0);
+    g = (g == 0) ? 1 : 0;
 }

src/ansi-c/ansi_c_entry_point.cpp

@@ -22,13 +22,25 @@ Author: Daniel Kroening, kroening@kroening.com
 #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())!=
@@ -447,7 +458,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_entry_point.h

@@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 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

@@ -27,11 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #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" };
@@ -132,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(),
-     wrap_entry_point_in_while()))
+  if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
   {
     return true;
   }