module Dyncall: sig
.. end
Returns an property identifier for the precondition.
val pp_calls : Format.formatter -> Cil_types.kernel_function list -> unit
val property : kf:Cil_types.kernel_function ->
?bhv:string ->
stmt:Cil_types.stmt -> calls:Cil_types.kernel_function list -> Property.t
Returns an property identifier for the precondition.
val get : ?bhv:string -> Cil_types.stmt -> Cil_types.kernel_function list
Returns empty list if there is no specified dynamic call.
val compute : unit -> unit
Forces computation of dynamic calls.
Otherwise, they are computed lazily on get
.
Requires -wp-dynamic
.