Add violation node for the memory safety benchmarks

We must not filter out generated assertions for memory leaks.

Author: lucasccordeiro

src/goto-programs/graphml_witness.cpp

@@ -11,9 +11,10 @@ Author: Daniel Kroening
 
 #include "graphml_witness.h"
 
+#include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
-#include <util/arith_tools.h>
+#include <util/cprover_prefix.h>
 #include <util/prefix.h>
 #include <util/ssa_expr.h>
 
@@ -189,7 +190,14 @@ static bool filter_out(
      source_location.get_file().empty() ||
      source_location.is_built_in() ||
      source_location.get_line().empty())
-    return true;
+  {
+    const irep_idt id = source_location.get_function();
+    // Do not filter out assertions in functions the name of which starts with
+    // CPROVER_PREFIX, because we need to maintain those as violation nodes:
+    // these are assertions generated, for examples, for memory leaks.
+    if(!has_prefix(id2string(id), CPROVER_PREFIX) || !it->is_assert())
+      return true;
+  }
 
   return false;
 }