Module Dyncall

module Dyncall: sig .. end
Returns an property identifier for the precondition.

val find_call : Logic_typing.typing_context ->
Cil_types.location -> string -> Cil_types.logic_var
val typecheck : string ->
typing_context:Logic_typing.typing_context ->
loc:Cil_types.location ->
(Cil_types.identified_predicate, 'a) Cil_types.behavior ->
Logic_ptree.lexpr list -> unit
val get_call : Cil_types.term -> Cil_types.kernel_function
val either : Cil_types.location ->
Cil_types.predicate Cil_types.named list ->
Cil_types.predicate Cil_types.named
val get_called_kf : Cil_types.identified_predicate -> Cil_types.kernel_function list
val get_calls : string ->
(Cil_types.identified_predicate, 'a) Cil_types.behavior list ->
(string * Kernel_function.t list) list
val pp_calls : Format.formatter -> Kernel_function.t list -> unit
module PInfo: sig .. end
module Point: Datatype.Pair_with_collections(Datatype.String)(Cil_datatype.Stmt)(PInfo)
module Calls: Datatype.List(Kernel_function)
module CInfo: sig .. end
module CallPoints: State_builder.Hashtbl(Point.Hashtbl)(Calls)(CInfo)
val property : kf:Cil_types.kernel_function ->
?bhv:string ->
stmt:Cil_types.stmt ->
calls:Kernel_function.t list -> Property.identified_property
Returns an property identifier for the precondition.
val dkey : Log.category
class dyncall : object .. end
val once : bool Pervasives.ref
val compute : unit -> unit
Forces computation of dynamic calls. Otherwize, they are computed lazily on get. Requires -wp-dynamic.
val get : ?bhv:Datatype.String.t -> Cil_datatype.Stmt.t -> CallPoints.data
Returns empty list if there is no specified dynamic call.
val register : unit -> unit