From f071cbac58c8a321bb9db704c6af576519e13789 Mon Sep 17 00:00:00 2001
From: Viktor Malik <viktor.malik@gmail.com>
Date: Sat, 28 Nov 2020 11:18:50 +0100
Subject: [PATCH 1/3] Do not allow calls to atexit in competition mode

The function is not supported yet - assert if it is used.
---
 src/2ls/2ls_parse_options.cpp  |  3 +++
 src/2ls/2ls_parse_options.h    |  1 +
 src/2ls/preprocessing_util.cpp | 20 ++++++++++++++++++++
 3 files changed, 24 insertions(+)

diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp
index 24b30bf17..64106cf48 100644
--- a/src/2ls/2ls_parse_options.cpp
+++ b/src/2ls/2ls_parse_options.cpp
@@ -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"))
     {
diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h
index 3b617893b..d3eb6862a 100644
--- a/src/2ls/2ls_parse_options.h
+++ b/src/2ls/2ls_parse_options.h
@@ -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
diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp
index a906678dd..59f1e29a1 100644
--- a/src/2ls/preprocessing_util.cpp
+++ b/src/2ls/preprocessing_util.cpp
@@ -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");
+      }
+    }
+  }
+}

From c0a5464e25cc726d331b87e7de016cfbc1a75281 Mon Sep 17 00:00:00 2001
From: Viktor Malik <viktor.malik@gmail.com>
Date: Tue, 8 Dec 2020 15:34:14 +0100
Subject: [PATCH 2/3] Update CBMC

Contains updates of generated witnesses. These are mainly fixes to
comply with the witness syntax required by SV-COMP (and checked by the
WitnessLint tool).

The CBMC branch is 2ls-prerequisites-0.9.1
---
 lib/cbmc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/cbmc b/lib/cbmc
index 5e5bc6c13..7ac49c6c1 160000
--- a/lib/cbmc
+++ b/lib/cbmc
@@ -1 +1 @@
-Subproject commit 5e5bc6c1324691ec35953596263742cc42373ed4
+Subproject commit 7ac49c6c1d53c7689d586b54945949fd3b8ad51e

From f56f67939685b43479cbb519769056d6a0f90cf2 Mon Sep 17 00:00:00 2001
From: Viktor Malik <viktor.malik@gmail.com>
Date: Fri, 11 Dec 2020 08:40:13 +0100
Subject: [PATCH 3/3] Version 0.9.1

Contains mainly fixes for SV-COMP'21.
---
 src/2ls/version.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/2ls/version.h b/src/2ls/version.h
index 33c465402..467e36dc8 100644
--- a/src/2ls/version.h
+++ b/src/2ls/version.h
@@ -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