sig
type can_goto = Cgo_break of int | Cgo_continue of int | Cgo_return
type fld_assignments = (Exp.exp * Misc.component * Exp.exp) list
type read_memory_order =
Crmo_nonatomic
| Crmo_relaxed
| Crmo_acquire
| Crmo_seq_cst
type write_memory_order =
Cwmo_nonatomic
| Cwmo_relaxed of (Misc.component * Misc.component * Exp.exp list) option
| Cwmo_release of (Misc.component * Misc.component * Exp.exp list) option
| Cwmo_seq_cst of (Misc.component * Misc.component * Exp.exp list) option
type cas_memory_order =
Ccmo_seq_cst
| Ccmo_rel_acq
| Ccmo_release
| Ccmo_acquire
| Ccmo_relaxed
type fun_info = {
fun_param : Exp.Id.t list * Exp.Id.t list;
fun_modif : Exp.IdSet.t;
fun_pre : Assertions.cprop;
fun_post : Assertions.cprop;
fun_loc : Location.t;
}
type can_stmt = {
can_st_desc : Commands.can_st_desc;
mutable can_st_lv : Exp.IdSet.t;
can_st_loc : Location.t;
}
and can_cmd = Commands.can_stmt list
and can_st_desc =
Cst_nondet of Commands.can_cmd * Commands.can_cmd
| Cst_kill of Exp.IdSet.t
| Cst_assign of Exp.Id.t * Exp.exp
| Cst_fldlookup of Misc.component list * Exp.Id.t * Exp.exp *
Misc.component * Commands.read_memory_order
| Cst_fldassign of Misc.component list * Commands.fld_assignments *
(string * Assertions.cprop) list Pervasives.ref *
Commands.write_memory_order
| Cst_cas of Misc.component list * Exp.Id.t * Exp.exp * Misc.component *
Exp.exp * Exp.exp * Commands.cas_memory_order *
Commands.read_memory_order
| Cst_new of Exp.Id.t * Exp.exp
| Cst_dispose of Exp.exp * Exp.exp
| Cst_pfcall of
(Exp.Id.t option * string * Commands.fun_info * Exp.Id.t list *
Exp.exp list)
list
| Cst_fcall2 of Exp.IdSet.t * Assertions.cprop * Assertions.cprop *
string
| Cst_assume of Assertions.cprop
| Cst_assume_exp of Exp.exp
| Cst_assert_exp of Exp.exp
| Cst_interfere of Misc.component * string
| Cst_stabilize of Misc.component
| Cst_action_begin of Misc.component * Assertions.cprop *
Assertions.cprop * Assertions.cprop * Exp.IdSet.t
| Cst_action_end of Misc.component * Exp.IdSet.t
| Cst_loop of Commands.can_cmd * Assertions.cprop option
| Cst_goto of Commands.can_goto
| Cst_comment of string
type can_entailment =
Assertions.cprop * Commands.can_cmd * Commands.can_cmd *
Assertions.cprop * Exp.IdSet.t * Location.t
type res_init =
Cri_inv of Assertions.cprop * Location.t
| Cri_code of Exp.IdSet.t * Commands.can_cmd * Location.t
val mk_cmd : Commands.can_st_desc -> Location.t -> Commands.can_cmd
val mk_assume : Exp.exp -> Location.t -> Commands.can_cmd
val mk_loop :
Commands.can_cmd ->
Assertions.cprop option -> Location.t -> Exp.IdSet.t -> Commands.can_cmd
val mk_nondet :
Commands.can_cmd -> Commands.can_cmd -> Location.t -> Commands.can_cmd
val cmd_copy : Commands.can_cmd -> Commands.can_cmd
val cmd_clear_copy : Commands.can_cmd -> Commands.can_cmd
val actlr_clear : (string * Commands.can_entailment) list -> unit
val actlr_iter :
(string * Assertions.cprop -> unit) ->
(string * Commands.can_entailment) list -> unit
val actlr_upd :
(Assertions.cprop -> Assertions.cprop) ->
(string * Commands.can_entailment) list -> unit
val actlr_print : (string * Commands.can_entailment) list -> unit
val ident_lin_res : Exp.Id.t
val linear_fun_pre : Assertions.cprop
val linear_fun_post : Assertions.cprop
val linear_parse_spec :
Commands.can_cmd -> Commands.can_cmd list * Commands.can_cmd list
val insert_pure_code :
Commands.can_cmd -> Commands.can_cmd -> Commands.can_cmd
val pp_cmd : Format.formatter -> Commands.can_cmd -> unit
val pp_linear_annot : Format.formatter -> Commands.can_cmd -> unit
val mark_live_vars : Exp.IdSet.t -> Commands.can_cmd -> unit
val insert_kill_dead_vars :
Commands.can_cmd -> Exp.IdSet.t -> Commands.can_cmd
val clarify_cmd : Commands.can_cmd -> Commands.can_cmd
val actlr_merge_linear :
(Assertions.cprop -> Commands.can_cmd -> 'a) ->
('a -> Assertions.cprop -> Assertions.cprop) ->
Commands.can_cmd ->
string * Commands.can_entailment ->
(string * Commands.can_entailment) list
val left_mover_optimization :
(string * Commands.can_entailment) list ->
(string * Commands.can_entailment) list
val add_prophecy : Commands.can_cmd -> Commands.can_cmd
val map_cmd : Exp.subst -> Commands.can_cmd -> Commands.can_cmd
val cmd_fcall_concat :
Commands.can_cmd -> Commands.can_cmd -> Commands.can_cmd
end