Factor out memory leak instrumentation into separate function

Author: peterschrammel

src/analyses/goto_check.cpp

@@ -103,6 +103,7 @@ class goto_checkt
 
   void bounds_check(const index_exprt &, const guardt &);
   void div_by_zero_check(const div_exprt &, const guardt &);
+  void memory_leak_check(const irep_idt &function_id);
   void mod_by_zero_check(const mod_exprt &, const guardt &);
   void undefined_shift_check(const shift_exprt &, const guardt &);
   void pointer_rel_check(const exprt &, const guardt &);
@@ -1515,6 +1516,30 @@ void goto_checkt::rw_ok_check(exprt &expr)
   }
 }
 
+void goto_checkt::memory_leak_check(const irep_idt &function_id)
+{
+  const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak");
+  const symbol_exprt leak_expr = leak.symbol_expr();
+
+  // add self-assignment to get helpful counterexample output
+  goto_programt::targett t = new_code.add_instruction();
+  t->make_assignment();
+  t->code = code_assignt(leak_expr, leak_expr);
+
+  source_locationt source_location;
+  source_location.set_function(function_id);
+
+  equal_exprt eq(leak_expr, null_pointer_exprt(to_pointer_type(leak.type)));
+
+  add_guarded_claim(
+    eq,
+    "dynamically allocated memory never freed",
+    "memory-leak",
+    source_location,
+    eq,
+    guardt());
+}
+
 void goto_checkt::goto_check(
   goto_functiont &goto_function,
   const irep_idt &_mode)
@@ -1713,30 +1738,11 @@ void goto_checkt::goto_check(
     }
     else if(i.is_end_function())
     {
-      if(i.function==goto_functionst::entry_point() &&
-         enable_memory_leak_check)
+      if(
+        i.function == goto_functionst::entry_point() &&
+        enable_memory_leak_check)
       {
-        const symbolt &leak=ns.lookup(CPROVER_PREFIX "memory_leak");
-        const symbol_exprt leak_expr=leak.symbol_expr();
-
-        // add self-assignment to get helpful counterexample output
-        goto_programt::targett t=new_code.add_instruction();
-        t->make_assignment();
-        t->code=code_assignt(leak_expr, leak_expr);
-
-        source_locationt source_location;
-        source_location.set_function(i.function);
-
-        equal_exprt eq(
-          leak_expr,
-          null_pointer_exprt(to_pointer_type(leak.type)));
-        add_guarded_claim(
-          eq,
-          "dynamically allocated memory never freed",
-          "memory-leak",
-          source_location,
-          eq,
-          guardt());
+        memory_leak_check(i.function);
       }
     }