why3 1.0.0 · OCaml Package

type struct_def = string * (string * ty) list

and ty =

and names = ty * (Ident.ident * expr) list

and name = ty * Ident.ident * expr

and proto = ty * (ty * Ident.ident) list

and binop =

and unop =

and expr =

and constant =

type stmt =

and include_kind =

and definition =

and body = definition list * stmt

type file = definition list

exception NotAValue

val is_nop : stmt -> bool

val is_true : stmt -> bool

val is_false : stmt -> bool

val one_stmt : stmt -> bool

val assignify : expr -> stmt -> stmt

val get_last_expr : stmt -> stmt * expr

val propagate_in_expr : Ident.ident -> expr -> expr -> expr

val propagate_in_stmt : Ident.ident -> expr -> stmt -> stmt

val propagate_in_def : Ident.ident -> expr -> definition -> definition * bool

val propagate_in_block : Ident.ident -> expr -> body -> body

val is_empty_block : stmt -> bool

val block_of_expr : expr -> 'a list * stmt

val flatten_defs : definition list -> stmt -> definition list * stmt

val group_defs_by_type : definition list -> definition list

val elim_empty_blocks : stmt -> stmt

val elim_nop : stmt -> stmt

val add_to_last_call : expr list -> stmt -> stmt

val stmt_of_list : stmt list -> stmt

val is_expr : stmt -> bool

val simplify_expr : ('a list * stmt) -> expr

val simplify_cond : ('a list * stmt) -> 'a list * stmt

package why3