Move AfterConfig.run to after the autotuner

goblint · Nov 22, 2023 · c5cda33 · c5cda33
1 parent 17ebe80
commit c5cda33
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -1056,7 +1056,13 @@ struct
             );
             (* Warn if any of the addresses contains a non-local and non-global variable *)
             if AD.exists (function
-                | AD.Addr.Addr (v, _) -> not (CPA.mem v st.cpa) && not (is_global a v)
+                | AD.Addr.Addr (v, _) ->
+                  (M.tracel "wtf" "checking for %a\n" CilType.Varinfo.pretty v;
+                   if v.vglob then
+                     (* this is OK *)
+                     false
+                   else
+                     (not (CPA.mem v st.cpa)) || WeakUpdates.mem v st.weak)
                 | _ -> false
               ) adr then (
               AnalysisStateUtil.set_mem_safety_flag InvalidDeref;

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
@@ -191,10 +191,10 @@ let handle_flags () =
 
 let handle_options () =
   check_arguments ();
-  AfterConfig.run ();
   Sys.set_signal (GobSys.signal_of_string (get_string "dbg.solver-signal")) Signal_ignore; (* Ignore solver-signal before solving (e.g. MyCFG), otherwise exceptions self-signal the default, which crashes instead of printing backtrace. *)
   if AutoTune.isActivated "memsafetySpecification" && get_string "ana.specification" <> "" then
     AutoTune.focusOnMemSafetySpecification ();
+  AfterConfig.run ();
   Cilfacade.init_options ();
   handle_flags ()