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