module Generator: sig
.. end
class type computer = object
.. end
val compute_ip : < add_lemma : LogicUsage.logic_lemma -> unit;
add_strategy : WpStrategy.strategy -> unit; compute : 'a Bag.t; .. > ->
Property.t -> 'a Bag.t
type
functions =
| |
F_All |
| |
F_List of string list |
| |
F_Skip of string list |
val iter_kf : (Cil_types.kernel_function -> unit) ->
Cil_types.kernel_function option -> unit
val iter_fct : (Kernel_function.t -> unit) -> functions -> unit
val add_kf : < add_strategy : WpStrategy.strategy -> unit; .. > ->
?bhv:string list -> ?prop:string list -> Kernel_function.t -> unit
val compute_kf : < add_strategy : WpStrategy.strategy -> unit; compute : 'a; .. > ->
?kf:Kernel_function.t -> ?bhv:string list -> ?prop:string list -> unit -> 'a
val do_lemmas : functions -> bool
val compute_selection : < add_lemma : LogicUsage.logic_lemma -> unit;
add_strategy : WpStrategy.strategy -> unit; compute : 'a; .. > ->
?fct:functions ->
?bhv:string list -> ?prop:string list -> unit -> 'a
val compute_call : < add_strategy : WpStrategy.strategy -> unit; compute : 'a; .. > ->
Cil_types.stmt -> 'a