sig
type myaction =
string * Pure.t * Assertions.can_spatial * Assertions.can_spatial *
Assertions.can_spatial
type stab_env = {
st_prover : Assertions.prover;
st_abstraction : Genarith.abstraction;
st_lin_hook : Assertions.uform list -> Assertions.uform list;
st_lin_exit : Assertions.uform list -> unit;
}
type guar_env = {
mutable ge_actions : (Misc.component * Actions.myaction) list;
mutable ge_changed : bool;
}
val mk_guar_env : unit -> Actions.guar_env
val verbose : int Pervasives.ref
val remember_result_hack : bool Pervasives.ref
val lock_abstraction_heuristic : bool Pervasives.ref
val args : (Arg.key * Arg.spec * Arg.doc) list
val stabilisation_iterations : int Pervasives.ref
val pp_actions : (Misc.component * Actions.myaction) list -> unit
val make_stable :
Actions.stab_env ->
Assertions.cprop -> Assertions.act list -> Assertions.cprop
val stabilize :
Actions.stab_env ->
Misc.component * Assertions.act list -> Genarith.eprop -> Genarith.eprop
val register_guarantee :
Actions.guar_env ->
Assertions.prover ->
Genarith.abstraction ->
Exp.IdSet.t ->
Exp.IdSet.t ->
(string * Assertions.cprop) list Pervasives.ref ->
Misc.component ->
Assertions.cprop -> Assertions.cprop -> Assertions.cprop -> unit
val update_res_ht :
Actions.guar_env ->
(Misc.component, Assertions.act list * Assertions.act list) Hashtbl.t ->
unit
end