|
|
@ -224,9 +224,20 @@ end
|
|
|
|
functor followed by normalization wrt the unification found between abstract locations so it's
|
|
|
|
functor followed by normalization wrt the unification found between abstract locations so it's
|
|
|
|
convenient to define stacks as elements of this domain. *)
|
|
|
|
convenient to define stacks as elements of this domain. *)
|
|
|
|
module Stack = struct
|
|
|
|
module Stack = struct
|
|
|
|
include AbstractDomain.Map
|
|
|
|
module VarAddress = struct
|
|
|
|
(Var)
|
|
|
|
include Var
|
|
|
|
(struct
|
|
|
|
|
|
|
|
|
|
|
|
let pp f var =
|
|
|
|
|
|
|
|
let pp_ampersand f = function
|
|
|
|
|
|
|
|
| ProgramVar _ ->
|
|
|
|
|
|
|
|
F.pp_print_string f "&"
|
|
|
|
|
|
|
|
| LogicalVar _ ->
|
|
|
|
|
|
|
|
()
|
|
|
|
|
|
|
|
in
|
|
|
|
|
|
|
|
F.fprintf f "%a%a" pp_ampersand var Var.pp var
|
|
|
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
module ValueDomain = struct
|
|
|
|
type t = AbstractAddress.t
|
|
|
|
type t = AbstractAddress.t
|
|
|
|
|
|
|
|
|
|
|
|
let ( <= ) ~lhs ~rhs = AbstractAddress.equal lhs rhs
|
|
|
|
let ( <= ) ~lhs ~rhs = AbstractAddress.equal lhs rhs
|
|
|
@ -236,7 +247,16 @@ module Stack = struct
|
|
|
|
let widen ~prev ~next ~num_iters:_ = join prev next
|
|
|
|
let widen ~prev ~next ~num_iters:_ = join prev next
|
|
|
|
|
|
|
|
|
|
|
|
let pp = AbstractAddress.pp
|
|
|
|
let pp = AbstractAddress.pp
|
|
|
|
end)
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
include AbstractDomain.Map (VarAddress) (ValueDomain)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let pp fmt m =
|
|
|
|
|
|
|
|
let pp_item fmt (var_address, v) =
|
|
|
|
|
|
|
|
F.fprintf fmt "%a=%a" VarAddress.pp var_address ValueDomain.pp v
|
|
|
|
|
|
|
|
in
|
|
|
|
|
|
|
|
PrettyPrintable.pp_collection ~pp_item fmt (bindings m)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let compare = compare AbstractAddress.compare
|
|
|
|
let compare = compare AbstractAddress.compare
|
|
|
|
end
|
|
|
|
end
|
|
|
|