sig
class type computer =
object
method add_lemma : LogicUsage.logic_lemma -> unit
method add_strategy : WpStrategy.strategy -> unit
method compute : Wpo.t Bag.t
method lemma : bool
method model : Model.t
end
type functions =
F_All
| F_List of Cil_datatype.Kf.Set.t
| F_Skip of Cil_datatype.Kf.Set.t
val compute_ip : Generator.computer -> Property.t -> Wpo.t Bag.t
val compute_call : Generator.computer -> Cil_types.stmt -> Wpo.t Bag.t
val compute_kf :
Generator.computer ->
?kf:Kernel_function.t ->
?bhv:string list -> ?prop:string list -> unit -> Wpo.t Bag.t
val compute_selection :
Generator.computer ->
?fct:Generator.functions ->
?bhv:string list -> ?prop:string list -> unit -> Wpo.t Bag.t
end