Add support for SV-COMP's valid-memcleanup property

src/autoTune.ml

@@ -227,6 +227,7 @@ let focusOnSpecification () =
   | ValidDeref
   | ValidMemtrack -> ()
   | MemorySafety -> () (* TODO: This is here for now just to complete the pattern match *)
+  | ValidMemcleanup -> ()
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound

src/framework/analysisState.ml

@@ -16,6 +16,9 @@ let svcomp_may_invalid_deref = ref false
 (** Whether an invalid memtrack happened *)
 let svcomp_may_invalid_memtrack = ref false
 
+(** Whether an invalid memcleanup happened *)
+let svcomp_may_invalid_memcleanup = ref false
+
 (** A hack to see if we are currently doing global inits *)
 let global_initialization = ref false
 

src/util/analysisStateUtil.ml

@@ -2,10 +2,12 @@ type mem_safety_violation =
   | InvalidFree
   | InvalidDeref
   | InvalidMemTrack
+  | InvalidMemcleanup
 
 let set_mem_safety_flag violation_type =
   if !AnalysisState.postsolving then
     match violation_type with
     | InvalidFree -> AnalysisState.svcomp_may_invalid_free := true
     | InvalidDeref -> AnalysisState.svcomp_may_invalid_deref := true
-    | InvalidMemTrack -> AnalysisState.svcomp_may_invalid_memtrack := true
+    | InvalidMemTrack -> AnalysisState.svcomp_may_invalid_memtrack := true
+    | InvalidMemcleanup -> AnalysisState.svcomp_may_invalid_memcleanup := true

src/witness/svcomp.ml

@@ -56,6 +56,7 @@ struct
         | ValidDeref -> "valid-deref"
         | ValidMemtrack -> "valid-memtrack"
         | MemorySafety -> "memory-safety" (* TODO: Currently here only to complete the pattern match *)
+        | ValidMemcleanup -> "valid-memcleanup"
       in
       "false(" ^ result_spec ^ ")"
     | Unknown -> "unknown"

src/witness/svcompSpec.ml

@@ -10,10 +10,12 @@ type t =
   | ValidDeref
   | ValidMemtrack
   | MemorySafety (* Internal property for use in Goblint; serves as a summary for ValidFree, ValidDeref and ValidMemtrack *)
+  | ValidMemcleanup
 
 let of_string s =
   let s = String.strip s in
-  let regexp = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )" in
+  let regexp_multiple = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )" in
+  let regexp_single = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )" in
   let regexp_negated = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in
   if Str.string_match regexp_negated s 0 then
     let global_not = Str.matched_group 1 s in
@@ -28,7 +30,7 @@ let of_string s =
         UnreachCall f
       else
         failwith "Svcomp.Specification.of_string: unknown global not expression"
-  else if Str.string_match regexp s 0 then
+  else if Str.string_match regexp_multiple s 0 then
     let global1 = Str.matched_group 1 s in
     let global2 = Str.matched_group 2 s in
     let global3 = Str.matched_group 3 s in
@@ -43,6 +45,12 @@ let of_string s =
           ValidMemtrack *)
     else
       failwith "Svcomp.Specification.of_string: unknown global expression"
+  else if Str.string_match regexp_single s 0 then
+    let global = Str.matched_group 1 s in
+    if global = "valid-memcleanup" then
+      ValidMemcleanup
+    else
+      failwith "Svcomp.Specification.of_string: unknown global expression"
   else
     failwith "Svcomp.Specification.of_string: unknown expression"
 
@@ -72,5 +80,6 @@ let to_string spec =
     | ValidDeref -> "valid-deref", false
     | ValidMemtrack -> "valid-memtrack", false
     | MemorySafety -> "memory-safety", false (* TODO: That's false, it's currently here just to complete the pattern match *)
+    | ValidMemcleanup -> "valid-memcleanup", false
   in
   print_output spec_str is_neg

src/witness/witness.ml

@@ -625,6 +625,36 @@ struct
         in
         (module TaskResult:WitnessTaskResult)
       )
+    | ValidMemcleanup ->
+      let module TrivialArg =
+      struct
+        include Arg
+        let next _ = []
+      end
+      in
+      if not !AnalysisState.svcomp_may_invalid_memcleanup then (
+        let module TaskResult =
+        struct
+          module Arg = Arg
+          let result = Result.True
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      ) else (
+        let module TaskResult =
+        struct
+          module Arg = TrivialArg
+          let result = Result.Unknown
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      )
 
 
   let write entrystates =