diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 61d28fc505..0dcf7cfb45 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -613,7 +613,7 @@ struct if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then RD.cil_exp_of_lincons1 lincons1 |> Option.map e_inv - |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp) && InvariantCil.exp_is_in_scope scope exp) + |> Option.filter (InvariantCil.exp_is_suitable ~scope) else None ) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 992b7fb587..9e22fff21c 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -733,7 +733,7 @@ struct (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *) if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then RD.cil_exp_of_lincons1 lincons1 - |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp)) + |> Option.filter (InvariantCil.exp_is_suitable ?scope:None) else None ) diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 3d3808c7b1..5597a67e9b 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -28,7 +28,7 @@ struct if B.mem MyCFG.unknown_exp s then a else ( - let s' = B.filter (fun x -> not (InvariantCil.exp_contains_tmp x) && InvariantCil.exp_is_in_scope scope x && not (is_str_constant x)) s in + let s' = B.filter (fun x -> InvariantCil.exp_is_suitable ~scope x && not (is_str_constant x)) s in if B.cardinal s' >= 2 then ( (* instead of returning quadratically many pairwise equalities from a cluster, output linear number of equalities with just one expression *) diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index 54dbb5cdfe..6f234cce50 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -1364,7 +1364,7 @@ struct Cilfacade.mkCast ~e ~newt:(TPtr (TVoid [], [])) in let i = - if InvariantCil.(not (exp_contains_tmp c_exp) && exp_is_in_scope scope c_exp && not (var_is_tmp vi) && var_is_in_scope scope vi && not (var_is_heap vi)) then + if InvariantCil.(exp_is_suitable ~scope c_exp && var_is_suitable ~scope vi && not (var_is_heap vi)) then try let addr_exp = AddrOf (Var vi, offset) in (* AddrOf or Lval? *) let addr_exp, c_exp = if typeSig (Cilfacade.typeOf addr_exp) <> typeSig (Cilfacade.typeOf c_exp) then @@ -1395,7 +1395,7 @@ struct | Addr.NullPtr -> let i = let addr_exp = integer 0 in - if InvariantCil.(not (exp_contains_tmp c_exp) && exp_is_in_scope scope c_exp) then + if InvariantCil.exp_is_suitable ~scope c_exp then Invariant.of_exp Cil.(BinOp (Eq, c_exp, addr_exp, intType)) else Invariant.none @@ -1417,13 +1417,13 @@ struct and vd_invariant ~vs ~offset ~lval = function | Compound.Int n -> let e = Lval lval in - if InvariantCil.(not (exp_contains_tmp e) && exp_is_in_scope scope e) then + if InvariantCil.exp_is_suitable ~scope e then ID.invariant e n else Invariant.none | Float n -> let e = Lval lval in - if InvariantCil.(not (exp_contains_tmp e) && exp_is_in_scope scope e) then + if InvariantCil.exp_is_suitable ~scope e then FD.invariant e n else Invariant.none diff --git a/src/cdomain/value/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml index d0194fcd75..da1f687360 100644 --- a/src/cdomain/value/domains/invariantCil.ml +++ b/src/cdomain/value/domains/invariantCil.ml @@ -90,6 +90,38 @@ let exp_contains_tmp e = ignore (visitCilExpr visitor e); !acc + +let fieldinfo_is_anon (fi: fieldinfo) = + String.starts_with ~prefix:"__annonCompField" fi.fname (* TODO: what if CIL-ed program explicitly has this? *) + +let rec offset_contains_anon_comp_offset = function + | NoOffset -> false + | Index (e, offs') -> offset_contains_anon_comp_offset offs' (* does not check e!, done by visitor *) + | Field (fi, offs') -> fieldinfo_is_anon fi || offset_contains_anon_comp_offset offs' + +class exp_contains_anon_comp_offset_visitor = object + inherit nopCilVisitor + method! voffs (offs: offset) = + if offset_contains_anon_comp_offset offs then + raise Stdlib.Exit + else + DoChildren (* recurse to Index offset expressions! *) +end +let exp_contains_anon_comp_offset = + let visitor = new exp_contains_anon_comp_offset_visitor in + fun e -> + match visitCilExpr visitor e with + | _ -> false + | exception Stdlib.Exit -> true + + +let var_is_suitable ?scope v = + not (var_is_tmp v) && GobOption.for_all (fun scope -> var_is_in_scope scope v) scope + +let exp_is_suitable ?scope e = + not (exp_contains_tmp e || exp_contains_anon_comp_offset e) && GobOption.for_all (fun scope -> exp_is_in_scope scope e) scope + + class exp_contains_anon_type_visitor = object inherit nopCilVisitor method! vtype (t: typ) = diff --git a/src/cdomains/c2poDomain.ml b/src/cdomains/c2poDomain.ml index 741b9c0d94..edb42f64c7 100644 --- a/src/cdomains/c2poDomain.ml +++ b/src/cdomains/c2poDomain.ml @@ -293,7 +293,7 @@ module D = struct let not_in_scope t = let var = T.get_var t in let var = Var.to_varinfo var in - InvariantCil.var_is_tmp var || not (InvariantCil.var_is_in_scope scope var) + not (InvariantCil.var_is_suitable ~scope var) in remove_terms not_in_scope cc end