sig
type global_env = {
g_prover : Assertions.prover;
g_abstraction : Genarith.abstraction;
mutable g_globals : Exp.IdSet.t;
g_pro_ht : (string, Tycheck.protocol_item) Hashtbl.t;
g_esc_ht : (string, Tycheck.escrow_item) Hashtbl.t;
g_fun_ht : (string, Commands.fun_info) Hashtbl.t;
g_res_ht :
(Misc.component, Assertions.act list * Assertions.act list) Hashtbl.t;
g_renv : (Misc.component, Assertions.cprop) Hashtbl.t;
g_guar : Actions.guar_env;
mutable g_actinf : bool;
mutable g_params : Exp.IdSet.t;
g_no_interf_hack : bool;
g_por_hack : bool;
mutable g_linear_pure_code : Commands.can_cmd;
g_linear_pre : Assertions.cprop option;
}
val all_fields : Misc.StringSet.t Pervasives.ref
val linear_symbexe :
Assertions.prover ->
Commands.can_stmt list ->
Exp.IdSet.t -> Assertions.uform list -> Assertions.uform list
val check_no_inference :
Symbsimp.global_env ->
(Misc.component * Commands.res_init) list ->
(string * Commands.can_entailment) list -> bool
val infer_actions_once :
Symbsimp.global_env ->
(Misc.component * Commands.res_init) list ->
(string * Commands.can_entailment) list -> bool
val infer_actions :
Symbsimp.global_env ->
(Misc.component * Commands.res_init) list ->
(string * Commands.can_entailment) list -> bool
val verbose : int Pervasives.ref
val args : (Arg.key * Arg.spec * Arg.doc) list
end