Merge pull request #145 from viktormalik/svcomp21-backport

SV-COMP'21 backport

Author: peterschrammel

lib/cbmc

@@ -1071,6 +1071,9 @@ bool twols_parse_optionst::process_goto_program(
     // remove returns (must be done after function pointer removal)
     remove_returns(goto_model);
 
+    if(options.get_bool_option("competition-mode"))
+      assert_no_atexit(goto_model);
+
     // now do full inlining, if requested
     if(options.get_bool_option("inline"))
     {

src/2ls/2ls_parse_options.cpp

@@ -208,6 +208,7 @@ class twols_parse_optionst:
   void memory_assert_info(goto_modelt &goto_model);
   void handle_freed_ptr_compare(goto_modelt &goto_model);
   void assert_no_builtin_functions(goto_modelt &goto_model);
+  void assert_no_atexit(goto_modelt &goto_model);
 };
 
 #endif

src/2ls/2ls_parse_options.h

@@ -811,3 +811,23 @@ void twols_parse_optionst::assert_no_builtin_functions(goto_modelt &goto_model)
     }
   }
 }
+
+/// Prevents usage of atexit function which is not supported, yet
+/// Must be called before inlining since it will lose the calls
+void twols_parse_optionst::assert_no_atexit(goto_modelt &goto_model)
+{
+  forall_goto_functions(f_it, goto_model.goto_functions)
+  {
+    forall_goto_program_instructions(i_it, f_it->second.body)
+    {
+      if(i_it->is_function_call())
+      {
+        auto &call=to_code_function_call(i_it->code);
+        if(!(call.function().id()==ID_symbol))
+          continue;
+        auto &name=id2string(to_symbol_expr(call.function()).get_identifier());
+        assert(name!="atexit");
+      }
+    }
+  }
+}

src/2ls/preprocessing_util.cpp

@@ -12,6 +12,6 @@ Author: Peter Schrammel
 #ifndef CPROVER_2LS_2LS_VERSION_H
 #define CPROVER_2LS_2LS_VERSION_H
 
-#define TWOLS_VERSION "0.9.0"
+#define TWOLS_VERSION "0.9.1"
 
 #endif