package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type float_type =
  1. | Plus_infinity
  2. | Minus_infinity
  3. | Plus_zero
  4. | Minus_zero
  5. | Not_a_number
  6. | Float_value of string * string * string
  7. | Float_hexa of string * float
val interp_float : ?interp:bool -> string -> string -> string -> float_type
type model_value =
  1. | String of string
  2. | Integer of string
  3. | Decimal of string * string
  4. | Fraction of string * string
  5. | Float of float_type
  6. | Boolean of bool
  7. | Array of model_array
  8. | Record of model_record
  9. | Proj of model_proj
  10. | Bitvector of string
  11. | Apply of string * model_value list
  12. | Unparsed of string
and arr_index = {
  1. arr_index_key : model_value;
  2. arr_index_value : model_value;
}
and model_array = {
  1. arr_others : model_value;
  2. arr_indices : arr_index list;
}
and model_proj = proj_name * model_value
and proj_name = string
and model_record = (field_name * model_value) list
and field_name = string
val array_create_constant : value:model_value -> model_array
val array_add_element : array:model_array -> index:model_value -> value:model_value -> model_array
val print_model_value : Format.formatter -> model_value -> unit
type model_element_kind =
  1. | Result
  2. | Old
  3. | Error_message
  4. | Other
type model_element_name = {
  1. men_name : string;
  2. men_kind : model_element_kind;
  3. men_attrs : Ident.Sattr.t;
}
type model_element = {
  1. me_name : model_element_name;
  2. me_value : model_value;
  3. me_location : Loc.position option;
  4. me_term : Term.term option;
}
val create_model_element : name:string -> value:model_value -> attrs:Ident.Sattr.t -> ?location:Loc.position -> ?term:Term.term -> unit -> model_element
type model
val is_model_empty : model -> bool
val default_model : model
val get_model_elements : model -> model_element list
val print_model : ?me_name_trans:(model_element_name -> string) -> print_attrs:bool -> Format.formatter -> model -> unit
val print_model_human : ?me_name_trans:(model_element_name -> string) -> Format.formatter -> model -> print_attrs:bool -> unit
val print_model_json : ?me_name_trans:(model_element_name -> string) -> ?vc_line_trans:(int -> string) -> Format.formatter -> model -> unit
val interleave_with_source : print_attrs:bool -> ?start_comment:string -> ?end_comment:string -> ?me_name_trans:(model_element_name -> string) -> model -> rel_filename:string -> source_code:string -> locations:(Loc.position * 'a) list -> string * (Loc.position * 'a) list
val model_for_positions_and_decls : model -> positions:Loc.position list -> model
type model_parser = string -> Printer.printer_mapping -> model
type raw_model_parser = Ident.ident Wstdlib.Mstr.t -> Ident.ident Wstdlib.Mstr.t -> (string * string) list Wstdlib.Mstr.t -> string list -> Ident.Sattr.t Wstdlib.Mstr.t -> string -> model_element list
val register_remove_field : ((Ident.Sattr.t * model_value) -> Ident.Sattr.t * model_value) -> unit
val register_model_parser : desc:Pp.formatted -> string -> raw_model_parser -> unit
val lookup_model_parser : string -> model_parser
val list_model_parsers : unit -> (string * Pp.formatted) list
OCaml

Innovation. Community. Security.