diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index eb162b81b..109168ac9 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -578,12 +578,13 @@ module PrePost = struct PulseDomain.InterprocAction.ViaCall {action= trace.action; f= Call proc_name; location} ; history= trace.history } - | MustBeValid _ - | WrittenTo _ | AddressOfCppTemporary (_, _) | AddressOfStackVariable (_, _, _) | Closure _ - | StdVectorReserve -> + | Constant _ + | MustBeValid _ + | StdVectorReserve + | WrittenTo _ -> attr diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index f9955f296..af42b0a77 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -255,6 +255,7 @@ module Attribute = struct | AddressOfCppTemporary of Var.t * ValueHistory.t | AddressOfStackVariable of Var.t * ValueHistory.t * Location.t | Closure of Typ.Procname.t + | Constant of Const.t | Invalid of Invalidation.t Trace.t | MustBeValid of unit InterprocAction.t | StdVectorReserve @@ -293,6 +294,8 @@ module Attribute = struct F.fprintf f "s&%a (%a) at %a" Var.pp var ValueHistory.pp history Location.pp location | Closure pname -> Typ.Procname.pp f pname + | Constant c -> + F.fprintf f "=%a" (Const.pp Pp.text) c | Invalid invalidation -> (Trace.pp Invalidation.pp) f invalidation | MustBeValid action -> diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index 8cae2c2ea..7db9cca01 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -84,6 +84,7 @@ module Attribute : sig | AddressOfCppTemporary of Var.t * ValueHistory.t | AddressOfStackVariable of Var.t * ValueHistory.t * Location.t | Closure of Typ.Procname.t + | Constant of Const.t | Invalid of Invalidation.t Trace.t | MustBeValid of unit InterprocAction.t | StdVectorReserve diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 3c6b2adcb..d32016d1b 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -146,7 +146,12 @@ let eval location exp0 astate = Closures.record location name (List.rev rev_captured) astate | Cast (_, exp') -> eval exp' astate - | Sizeof _ | UnOp _ | BinOp _ | Exn _ | Const _ -> + | Const c -> + (* TODO: make identical const the same address *) + let addr = AbstractAddress.mk_fresh () in + let astate = Memory.add_attribute addr (Constant c) astate in + Ok (astate, (addr, [])) + | Sizeof _ | UnOp _ | BinOp _ | Exn _ -> Ok (astate, (AbstractAddress.mk_fresh (), (* TODO history *) [])) in eval exp0 astate