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