sig
type p_type = string
type p_read_memory_order =
Prmo_nonatomic
| Prmo_relaxed
| Prmo_acquire
| Prmo_seq_cst
and p_write_memory_order =
Pwmo_nonatomic
| Pwmo_relaxed of (string * string * Parsetree.a_expression list) option
| Pwmo_release of (string * string * Parsetree.a_expression list) option
| Pwmo_seq_cst of (string * string * Parsetree.a_expression list) option
and p_cas_memory_order =
Pcmo_seq_cst
| Pcmo_rel_acq
| Pcmo_release
| Pcmo_acquire
| Pcmo_relaxed
and p_expression = {
pexp_desc : Parsetree.p_expression_desc;
pexp_loc : Location.t;
}
and p_expression_desc =
Pexp_ident of string
| Pexp_num of int
| Pexp_bool of bool
| Pexp_prefix of string * Parsetree.p_expression
| Pexp_infix of string * Parsetree.p_expression * Parsetree.p_expression
| Pexp_cast of Parsetree.p_expression * Parsetree.p_type
| Pexp_fld of Parsetree.p_expression * Misc.component *
Parsetree.p_read_memory_order
| Pexp_cas of Parsetree.p_expression * Misc.component *
Parsetree.p_expression * Parsetree.p_expression *
Parsetree.p_cas_memory_order * Parsetree.p_read_memory_order
| Pexp_new of Parsetree.p_type * Parsetree.p_expression
| Pexp_fun of string * Parsetree.p_expression list
| Pexp_fcall of string * Parsetree.actual_params
and actual_params =
Parsetree.p_expression list * Parsetree.p_expression list
and a_expression = Parsetree.p_expression
type dlink_kind = DL | XL
type a_proposition =
Aprop_exp of Parsetree.a_expression
| Aprop_node of Misc.component * Parsetree.a_expression *
(Misc.component * Parsetree.a_expression) list
| Aprop_indpred of string * (string * Location.t) list *
Parsetree.a_expression list * Location.t
| Aprop_ifthenelse of Parsetree.a_expression * Parsetree.a_proposition *
Parsetree.a_proposition
| Aprop_star of Parsetree.a_proposition * Parsetree.a_proposition
| Aprop_barbar of Parsetree.a_proposition * Parsetree.a_proposition
| Aprop_box of Misc.component * Parsetree.a_proposition
| Aprop_atomic_fld of Parsetree.a_expression * string * string *
string * Parsetree.a_expression list
| Aprop_escrow of string * Parsetree.a_expression list
| Aprop_token of Parsetree.a_expression
type a_invariant = Parsetree.a_proposition option
type p_statement = {
pstm_desc : Parsetree.p_statement_desc;
pstm_loc : Location.t;
}
and p_statement_desc =
Pstm_exp of Parsetree.p_expression
| Pstm_assign of string * Parsetree.p_expression option
| Pstm_fldassign of
(Parsetree.p_expression * Misc.component * Parsetree.p_expression)
list * Parsetree.p_write_memory_order
| Pstm_dispose of Parsetree.p_expression * Parsetree.p_expression
| Pstm_block of Parsetree.p_statement list
| Pstm_assume of Parsetree.p_expression
| Pstm_if of Parsetree.p_expression option * Parsetree.p_statement *
Parsetree.p_statement
| Pstm_while of Parsetree.a_invariant * Parsetree.p_expression option *
Parsetree.p_statement
| Pstm_atomic of Parsetree.p_expression * Parsetree.p_statement
| Pstm_withres of Misc.component * Parsetree.p_expression *
Parsetree.p_statement * string * Parsetree.p_expression list
| Pstm_action of Parsetree.p_statement * Misc.component * string *
Parsetree.p_expression list
| Pstm_parblock of
(string option * string * Parsetree.actual_params) list
| Pstm_interfere of Misc.component * string
| Pstm_return of Parsetree.p_expression option
| Pstm_break
| Pstm_continue
| Pstm_comment of string
type p_action =
string * (string * Location.t) list * Parsetree.a_proposition *
Parsetree.a_proposition * Parsetree.a_proposition *
Parsetree.p_statement list * Location.t
type p_vars = (string * Parsetree.p_type * Location.t) list
type p_state_after =
string * (string * Location.t) list * Parsetree.a_proposition *
Location.t
type p_protocol_state =
string * (string * Location.t) list * Parsetree.p_state_after list *
string * Parsetree.a_proposition * Location.t
type p_item =
Pdec_options of (string * string * Location.t) list
| Pdec_class of string * Parsetree.p_vars * Location.t
| Pdec_var of string * Parsetree.p_type * bool * Location.t
| Pdec_fun of string * Parsetree.p_type *
(Parsetree.p_vars * Parsetree.p_vars) *
(Parsetree.a_invariant * Parsetree.a_invariant) *
(Parsetree.p_vars * Parsetree.p_statement list) * bool * Location.t
| Pdec_resource of Misc.component * (string * Location.t) list *
Parsetree.a_invariant *
(Parsetree.p_vars * Parsetree.p_statement list) *
Parsetree.p_statement list option * Parsetree.p_action list *
Location.t
| Pdec_indpred of string * (string * Location.t) list *
Parsetree.a_proposition * Location.t
| Pdec_comment of string
| Pdec_protocol of string * Parsetree.p_protocol_state list * Location.t
| Pdec_escrow of string * (string * Location.t) list *
Parsetree.a_proposition * Parsetree.a_proposition * Location.t
type p_program = Parsetree.p_item list
val iter :
(Location.t -> Parsetree.p_statement_desc -> unit) ->
Parsetree.p_statement list -> unit
val a_prop_empty : Parsetree.a_proposition
val exp_is_pure : Parsetree.p_expression -> bool
end