diff --git a/src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml b/src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml index 62f30db64c..359e6b278d 100644 --- a/src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml +++ b/src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml @@ -14,16 +14,16 @@ let spec_module: (module MCPSpec) Lazy.t = struct include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil) let name () = "lin2vareq" - let branch ctx e b = + let branch man e b = if M.tracing then M.trace "lin2vareq" "Branching"; - let res = branch ctx e b in - let st = ctx.local in - let ask = Analyses.ask_of_ctx ctx in - let _ = assign_from_globals_wrapper ask ctx.global st e (fun d e' -> + let res = branch man e b in + let st = man.local in + let ask = Analyses.ask_of_man man in + let _ = assign_from_globals_wrapper ask man.global st e (fun d e' -> try let tcons = AD.tcons1_of_cil_exp ask d d.env e (not b) (no_overflow ask e) in - let constraintlist = AD.refine_value_domains ctx d tcons in - List.iter (fun e -> ctx.emit (Events.Assert e)) constraintlist; + let constraintlist = AD.refine_value_domains man d tcons in + List.iter (fun e -> man.emit (Events.Assert e)) constraintlist; d with _ -> d) in diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index b6cebe962e..ca33f56d96 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -710,7 +710,7 @@ struct let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov - let refine_value_domains (ctx:('a,'b,'c,'d) Analyses.ctx) t tcons = + let refine_value_domains (man:('a,'b,'c,'d) Analyses.man) t tcons = match t.d with | None -> [] | Some d ->