module Make: functor (
Abstract
:
Abstractions.S
) ->
functor (
Eva
:
Evaluation.S
with type value = Abstract.Val.t
and type origin = Abstract.Dom.origin
and type loc = Abstract.Loc.location
and type state = Abstract.Dom.t
) ->
sig
.. end
Parameters: |
Abstract |
: |
Abstractions.S
|
Eva |
: |
Evaluation.S with type value = Abstract.Val.t
and type origin = Abstract.Dom.origin
and type loc = Abstract.Loc.location
and type state = Abstract.Dom.t
|
|
val compute_from_entry_point : Cil_types.kernel_function -> lib_entry:bool -> unit
Compute a call to the main function.
val compute_from_init_state : Cil_types.kernel_function -> Abstract.Dom.t -> unit
Compute a call to the main function from the given initial state.
val initial_state : lib_entry:bool -> Abstract.Dom.t Eval.or_bottom