Module Actions

module Actions: sig .. end
Rely-guarantee actions

type myaction = string * Pure.t * Assertions.can_spatial * Assertions.can_spatial *
Assertions.can_spatial
action name, context pure, context spatial, action pre, action post
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 * myaction) list;
   mutable ge_changed : bool;
}
val mk_guar_env : unit -> guar_env

Configuration parameters & statistics


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
total number of iterations for all the calls to mk_stable_single
val pp_actions : (Misc.component * myaction) list -> unit

Stabilisation


val make_stable : stab_env ->
Assertions.cprop -> Assertions.act list -> Assertions.cprop
make_stable env cp rely returns a cp' such that cp |- cp' and stable_under cp rely
val stabilize : stab_env ->
Misc.component * Assertions.act list -> Genarith.eprop -> Genarith.eprop
Compute eq such that ep |- eq and stable_under ep rely

Action registration


val register_guarantee : 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
Add action cp_ctx | cp ~~> cq to the guarantee.
val update_res_ht : guar_env ->
(Misc.component, Assertions.act list * Assertions.act list) Hashtbl.t -> unit
Imprint | Data protection