From 5093b5dd90a6ec7aca4c541e007c7d4f3025b707 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 31 Oct 2023 17:25:11 +0200
Subject: [PATCH] Fix witness determine_result for memsafety

---
 src/witness/witness.ml | 64 ++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 61 insertions(+), 3 deletions(-)

diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 419185400c..dd829dd9e2 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -505,8 +505,66 @@ struct
         in
         (module TaskResult:WitnessTaskResult)
       )
-    | ValidFree
-    | ValidDeref
+    | ValidFree ->
+      let module TrivialArg =
+      struct
+        include Arg
+        let next _ = []
+      end
+      in
+      if not !AnalysisState.svcomp_may_invalid_free 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)
+      )
+    | ValidDeref ->
+      let module TrivialArg =
+      struct
+        include Arg
+        let next _ = []
+      end
+      in
+      if not !AnalysisState.svcomp_may_invalid_deref 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)
+      )
     | ValidMemtrack ->
       let module TrivialArg =
       struct
@@ -514,7 +572,7 @@ struct
         let next _ = []
       end
       in
-      if not !AnalysisState.svcomp_may_invalid_free && not !AnalysisState.svcomp_may_invalid_deref && not !AnalysisState.svcomp_may_invalid_memtrack then (
+      if not !AnalysisState.svcomp_may_invalid_memtrack then (
         let module TaskResult =
         struct
           module Arg = Arg