Module Generator

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