mallocFresh

Author: ge46lup

src/analyses/mallocFresh.ml

@@ -9,7 +9,12 @@ struct
   include Analyses.IdentitySpec
 
   (* must fresh variables *)
-  module D = SetDomain.Reverse (SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All variables" end)) (* need bot (top) for hoare widen *)
+  (*module D = SetDomain.Reverse (SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All variables" end)) (* need bot (top) for hoare widen *)
+  *)
+  module D = SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All variables" end)
+
+  
+  
   module C = D
 
   let name () = "mallocFresh"
@@ -21,7 +26,12 @@ struct
     match ask.f (MayPointTo (AddrOf lval)) with
     | ad when Queries.AD.is_top ad -> D.empty ()
     | ad when Queries.AD.exists (function
-        | Queries.AD.Addr.Addr (v,_) -> not (D.mem v local) && (v.vglob || ThreadEscape.has_escaped ask v)
+        (*| Queries.AD.Addr.Addr (v,_) -> not (D.mem v local) && (v.vglob || ThreadEscape.has_escaped ask v)*)
+        | Queries.AD.Addr.Addr (v,_) ->
+          if D.mem (v, false) local then
+            D.add (v, true) local  (* Invalidate the variable *)
+          else
+            local
         | _ -> false
       ) ad -> D.empty ()
     | _ -> local

src/common/util/cilfacade0.ml

@@ -30,6 +30,7 @@ let get_instrLoc = function
   | Set (_, _, loc, eloc) -> eloc_fallback ~eloc ~loc
   | Call (_, _, _, loc, eloc) -> eloc_fallback ~eloc ~loc
   | VarDecl (_, loc) -> loc
+  
 
 (** Get expression location for [Cil.stmt]. *)
 (* confusingly CIL.get_stmtLoc works on stmtkind instead *)

tests/practical/test_file

@@ -0,0 +1,26 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+void allocateMemory() {
+    int *ptr = malloc(sizeof(int));
+    
+    if (ptr != NULL) {
+        *ptr = 42;
+
+        // Your code that uses 'ptr'
+
+        printf("Value: %d\n", *ptr);
+
+        free(ptr);
+    } else {
+        fprintf(stderr, "Memory allocation failed.\n");
+    }
+}
+
+int main() {
+    allocateMemory();
+
+    // Additional code if needed
+
+    return 0;
+}