Disable unsupported operations in competition mode

For now, we disable memcpy as it is implemented via a CBMC built-in
operation that we do not support in 2LS, yet.

Author: viktormalik

src/ssa/local_ssa.cpp

@@ -51,6 +51,9 @@ void local_SSAt::build_SSA()
     build_function_call(i_it);
 //    build_unknown_objs(i_it);
     collect_record_frees(i_it);
+
+    if (options.get_bool_option("competition-mode"))
+      disable_unsupported_instructions(i_it);
   }
 
   // collect custom templates in loop heads
@@ -1644,3 +1647,13 @@ bool local_SSAt::can_reuse_symderef(
 
   return true;
 }
+
+void local_SSAt::disable_unsupported_instructions(locationt loc)
+{
+  if (loc->is_other())
+  {
+    auto st = loc->get_code().get_statement();
+    if(st=="array_copy" || st=="array_replace")
+      assert(false);
+  }
+}

src/ssa/local_ssa.h

@@ -271,6 +271,9 @@ class local_SSAt
   void build_assertions(locationt loc);
   void build_unknown_objs(locationt loc);
 
+  // competition-mode specific checks
+  void disable_unsupported_instructions(locationt loc);
+
   void collect_allocation_guards(const code_assignt &assign, locationt loc);
   void get_alloc_guard_rec(const exprt &expr, exprt old_guard);
   void collect_record_frees(locationt loc);