diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 84be8c7a19..518d4d88c6 100644 --- 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 index 82a19aa4ae..79b0d121f6 100644 --- 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 ()