why3 1.3.1 · OCaml Package

why3

type float_type =

| Plus_infinity
| Minus_infinity
| Plus_zero
| Minus_zero
| Not_a_number
| Float_value of string * string * string
| Float_hexa of string * float

val interp_float : ?interp:bool -> string -> string -> string -> float_type

type model_value =

| String of string
| Integer of string
| Decimal of string * string
| Fraction of string * string
| Float of float_type
| Boolean of bool
| Array of model_array
| Record of model_record
| Proj of model_proj
| Bitvector of string
| Apply of string * model_value list
| Unparsed of string

and arr_index = {

arr_index_key : model_value;
arr_index_value : model_value;

}

and model_array = {

arr_others : model_value;
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 =

| Result
| Old
| Error_message
| Other

type model_element_name = {

men_name : string;
men_kind : model_element_kind;
men_attrs : Ident.Sattr.t;

}

type model_element = {

me_name : model_element_name;
me_value : model_value;
me_location : Loc.position option;
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

package why3