sig
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
val convert_exp_se :
Convert.fun_info_ht ->
Misc.component list ->
Parsetree.p_expression ->
Commands.can_stmt list -> Commands.can_stmt list * Exp.exp
val convert_exp_list_se :
Convert.fun_info_ht ->
Misc.component list ->
Parsetree.p_expression list ->
Commands.can_stmt list -> Commands.can_stmt list * Exp.exp list
val convert_read_memory_order :
Parsetree.p_read_memory_order -> Commands.read_memory_order
val convert_cas_memory_order_se :
Convert.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 :
Convert.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 :
Convert.fun_info_ht ->
Misc.component list ->
Parsetree.p_expression -> Commands.can_stmt list * Commands.can_stmt list
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
end