forgot to pull

Author: Simon Tietz

src/analyses/accessAnalysis.ml

@@ -80,7 +80,7 @@ struct
       let ins, outs = Analyses.asm_extract_ins_outs ctx in
       let handle_in exp = access_one_top ctx Read false exp in
       List.iter handle_in ins;
-      let handle_out lval = access_one_top ~deref:true ctx Write false (AddrOf lval) in
+      let handle_out lval = access_one_top ctx Write false (AddrOf lval) in
       List.iter handle_out outs;
     end;
     ctx.local

src/analyses/base.ml

@@ -1229,9 +1229,8 @@ struct
             | JmpBuf (x, copied, invalid) ->
               if copied then
                 M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e;
-              (* M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a was modified by inline assembly. This is may lead to Undefined Behavior." d_exp e; *)
               if invalid then
-                M.warn ~category:(Behavior (Undefined Other)) "The jump target %a may have been altered in an inline assembly block." d_exp e;
+                M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a was modified by inline assembly. This is may lead to Undefined Behavior." d_exp e;
               x
             | Top
             | Bot ->

src/analyses/mallocFresh.ml

@@ -29,22 +29,13 @@ struct
   let assign ctx lval rval =
     assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
-    let is_relevant_variable v =
-      (* Check if the variable is a global variable *)
-      v.vglob
-    
-    let event ctx e octx =
-        match e with
-        | Events.Invalidate {lvals} ->
-          (* Perform invalidation for mallocFresh analysis *)
-          let updated_locals = List.fold_left (fun acc lval ->
-            (* Check if lval is relevant to mallocFresh analysis and update the domain accordingly *)
-            match lval with
-            | (Var v, _) when is_relevant_variable v -> D.remove v acc
-            | _ -> acc
-          ) ctx.local lvals in
-          updated_locals
-        | _ -> ctx.local  
+  let event ctx e octx =
+    match e with
+    | Events.Invalidate {lvals} ->
+      let ask = Analyses.ask_of_ctx ctx in
+      let handle_lval local lval = assign_lval ask lval local in
+      List.fold_left handle_lval ctx.local lvals
+    | _ -> ctx.local
 
   let combine_env ctx lval fexp f args fc au f_ask =
     ctx.local (* keep local as opposed to IdentitySpec *)

src/goblint.ml

@@ -61,7 +61,7 @@ let main () =
       (* This is run independant of the autotuner being enabled or not be sound for programs with longjmp *)
       AutoTune.activateLongjmpAnalysesWhenRequired ();
       if get_bool "ana.autotune.enabled" then AutoTune.chooseConfig file;
-      file |> do_analyze changeInfo; 
+      file |> do_analyze changeInfo;
       do_html_output ();
       do_gobview file;
       do_stats ();