Assert that no longjmp is used

Author: FrNecas

src/2ls/2ls_parse_options.cpp

@@ -1045,7 +1045,7 @@ bool twols_parse_optionst::process_goto_program(
     }
 
     if(options.get_bool_option("competition-mode"))
-      assert_no_builtin_functions(goto_model);
+      assert_no_unsupported_functions(goto_model);
 
     make_scanf_nondet(goto_model);
 

src/2ls/2ls_parse_options.h

@@ -185,7 +185,7 @@ class twols_parse_optionst:
   void remove_dead_goto(goto_modelt &goto_model);
   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_unsupported_functions(goto_modelt &goto_model);
   void assert_no_atexit(goto_modelt &goto_model);
   void fix_goto_targets(goto_modelt &goto_model);
   void make_assertions_false(goto_modelt &goto_model);

src/2ls/preprocessing_util.cpp

@@ -653,9 +653,12 @@ void twols_parse_optionst::handle_freed_ptr_compare(goto_modelt &goto_model)
   }
 }
 
-/// Add assertions preventing analysis of programs using GCC builtin functions
-/// that are not supported and can cause false results.
-void twols_parse_optionst::assert_no_builtin_functions(goto_modelt &goto_model)
+/// Fail if the program contains any functions that 2LS does not currently
+/// support. These include:
+///     - builtin gcc functions
+///     - longjmp (not supported by CBMC)
+void twols_parse_optionst::assert_no_unsupported_functions(
+  goto_modelt &goto_model)
 {
   forall_goto_program_instructions(
     i_it,
@@ -666,6 +669,7 @@ void twols_parse_optionst::assert_no_builtin_functions(goto_modelt &goto_model)
     assert(
       name.find("__builtin_")==std::string::npos &&
       name.find("__CPROVER_overflow")==std::string::npos);
+    assert(name!="longjmp" && name!="_longjmp" && name!="siglongjmp");
 
     if(i_it->is_assign())
     {