|
let sync ctx reason = |
|
(* After the solver is finished, store the results (for later comparison) *) |
|
if !AnalysisState.postsolving then begin |
|
let keep_local = GobConfig.get_bool "ana.relation.invariant.local" in |
|
let keep_global = GobConfig.get_bool "ana.relation.invariant.global" in |
|
|
|
(* filter variables *) |
|
let var_filter v = match RV.find_metadata v with |
|
| Some (Global _) -> keep_global |
|
| Some (Local _) -> keep_local |
|
| _ -> false |
|
in |
|
let st = RD.keep_filter ctx.local.rel var_filter in |
|
let old_value = PCU.RH.find_default results ctx.node (RD.bot ()) in |
|
let new_value = RD.join old_value st in |
|
PCU.RH.replace results ctx.node new_value; |
|
end; |
|
WideningTokens.with_local_side_tokens (fun () -> |
|
Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread]) |
|
) |
Here, the table results is always populated, even whenexp.relation.prec-dump is off, and results is never considered. This is likely not terribly expensive given casting to octagons only happens later, but still completely unnecessary.