module Make: functor (
Abstract
:
Abstractions.S
) ->
functor (
States
:
Powerset.S
with type state = Abstract.Dom.t
) ->
functor (
Logic
:
Transfer_logic.S
with type state = Abstract.Dom.t
and type states = States.t
) ->
sig
.. end
val treat_statement_assigns : Cil_types.assigns -> Abstract.Dom.t -> Abstract.Dom.t
val compute_using_specification : warn:bool ->
Cil_types.kinstr ->
(Abstract.Loc.location, Abstract.Val.t) Eval.call ->
Cil_types.spec -> Abstract.Dom.t -> Abstract.Dom.t list Eval.or_bottom