Module Convert

module Convert: sig .. end
Translate parse tree into the intermediate abstract syntax tree

exception Undef_non_pure_expression
exception Conversion_error of string * Location.t
type fun_info_ht = (string, Commands.fun_info) Hashtbl.t 
val convert_exp : Parsetree.p_expression -> Exp.exp
Convert a p_expression to a exp. Throws Undef_non_pure_expression if the expression contains indirections.
val convert_exp_se : fun_info_ht ->
Misc.component list ->
Parsetree.p_expression ->
Commands.can_stmt list -> Commands.can_stmt list * Exp.exp
convert_exp_se fun_ht pe stmts returns the read side-effects required for the indirections in pe and a exp representing pe
val convert_exp_list_se : fun_info_ht ->
Misc.component list ->
Parsetree.p_expression list ->
Commands.can_stmt list -> Commands.can_stmt list * Exp.exp list
convert_exp_list_se fun_ht pel stmts returns the read side-effects required for the indirections in pel and a exp list representing pel
val convert_read_memory_order : Parsetree.p_read_memory_order -> Commands.read_memory_order
val convert_cas_memory_order_se : fun_info_ht ->
Misc.component list ->
Parsetree.p_cas_memory_order ->
Commands.can_stmt list -> Commands.can_stmt list * Commands.cas_memory_order
val convert_write_memory_order_se : fun_info_ht ->
Misc.component list ->
Parsetree.p_write_memory_order ->
Commands.can_stmt list ->
Commands.can_stmt list * Commands.write_memory_order
val convert_assume_exp : fun_info_ht ->
Misc.component list ->
Parsetree.p_expression -> Commands.can_stmt list * Commands.can_stmt list
convert_assume_exp fun_ht e returns the statements required to evaluate assume e and assume (not e).
val convert_prop : Parsetree.a_proposition -> Location.t -> Assertions.cprop
val prop_to_ip_body : Parsetree.a_proposition -> Location.t -> (Pure.t * Assertions.cform) list
Imprint | Data protection