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 : string -> string -> string -> float_type
type model_value =
  1. | Integer of string
  2. | Decimal of string * string
  3. | Fraction of string * string
  4. | Float of float_type
  5. | Boolean of bool
  6. | Array of model_array
  7. | Record of model_record
  8. | Bitvector of string
  9. | Apply of string * model_value list
  10. | Unparsed of string
and arr_index = {
  1. arr_index_key : string;
  2. arr_index_value : model_value;
}
and model_array = {
  1. arr_others : model_value;
  2. arr_indices : arr_index list;
}
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:string -> 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 -> ?location:Loc.position -> ?term:Term.term -> unit -> model_element
type model
val is_model_empty : model -> bool
val default_model : model
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 model_to_string : print_attrs:bool -> ?me_name_trans:(model_element_name -> string) -> model -> string
val print_model_json : ?me_name_trans:(model_element_name -> string) -> ?vc_line_trans:(int -> string) -> Format.formatter -> model -> unit
val model_to_string_json : ?me_name_trans:(model_element_name -> string) -> ?vc_line_trans:(int -> string) -> model -> string
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 = Wstdlib.Sstr.t -> (string * string) list Wstdlib.Mstr.t -> string -> model_element list
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.