Module Model_parser

module Model_parser: sig .. end

Counter-example model values


type model_int = {
   int_value : BigInt.t;
   int_verbatim : string;
}
type model_dec = {
   dec_int : BigInt.t;
   dec_frac : BigInt.t;
   dec_verbatim : string;
}
type model_frac = {
   frac_nom : BigInt.t;
   frac_den : BigInt.t;
   frac_verbatim : string;
}
type model_bv = {
   bv_value : BigInt.t;
   bv_length : int;
   bv_verbatim : string;
}
type model_float_binary = {
   sign : model_bv;
   exp : model_bv;
   mant : model_bv;
}
type model_float = 
| Plus_infinity
| Minus_infinity
| Plus_zero
| Minus_zero
| Not_a_number
| Float_number of {
   hex : string option;
   binary : model_float_binary;
}
type model_value = 
| Boolean of bool
| String of string
| Integer of model_int
| Float of model_float
| Bitvector of model_bv
| Decimal of model_dec
| Fraction of model_frac
| Array of model_array
| Record of model_record
| Proj of model_proj
| Apply of string * model_value list
| Undefined
| Unparsed of string
type arr_index = {
   arr_index_key : model_value;
   arr_index_value : model_value;
}
type model_array = {
   arr_others : model_value;
   arr_indices : arr_index list;
}
type model_record = (field_name * model_value) list 
type model_proj = proj_name * model_value 
type proj_name = string 
type field_name = string 
val array_create_constant : value:model_value -> model_array

Creates constant array with all indices equal to the parameter value.

val array_add_element : array:model_array ->
index:model_value ->
value:model_value -> model_array

Adds an element to the array.

array : : the array to that the element will be added
index : : the index on which the element will be added.
value : : the value of the element to be added
val float_of_binary : model_float_binary -> model_float
val print_model_value : Stdlib.Format.formatter -> model_value -> unit
val debug_force_binary_floats : Debug.flag

Print all floats using bitvectors in JSON output for models

type model_element_kind = 
| Result
| Old
| At of string
| Error_message
| Loop_before
| Loop_previous_iteration
| Loop_current_iteration
| Other
type model_element_name = {
   men_name : string; (*

The name of the source-code element.

*)
   men_kind : model_element_kind; (*

The kind of model element.

*)
   men_attrs : Ident.Sattr.t;
}

Information about the name of the model element

type model_element = {
   me_name : model_element_name; (*

Information about the name of the model element

*)
   me_value : model_value; (*

Counter-example value for the element.

*)
   me_location : Loc.position option; (*

Source-code location of the element.

*)
   me_term : Term.term option; (*

Why term corresponding to the element.

*)
}

Counter-example model elements. Each element represents a counter-example for a single source-code element.

val create_model_element : name:string ->
value:model_value ->
attrs:Ident.Sattr.t -> model_element

Creates a counter-example model element.

name : : the name of the source-code element
value : : counter-example value for the element

Model definitions

type model 
val map_filter_model_elements : (model_element -> model_element option) ->
model -> model
val is_model_empty : model -> bool
val empty_model : model
val set_model_files : model ->
model_element list Wstdlib.Mint.t Wstdlib.Mstr.t ->
model

Querying the model

val get_model_elements : model -> model_element list
val get_model_term_loc : model -> Loc.position option
val get_model_term_attrs : model -> Ident.Sattr.t
val get_model_element : model ->
string -> Loc.position -> model_element option
val get_model_element_by_id : model -> Ident.ident -> model_element option
val get_model_element_by_loc : model -> Loc.position -> model_element option

Printing the model

val print_model : ?filter_similar:bool ->
?me_name_trans:(model_element_name -> string) ->
print_attrs:bool -> Stdlib.Format.formatter -> model -> unit

Prints the counter-example model

me_name_trans : the transformation of the model elements names. The input is information about model element name. The output is the name of the model element that should be displayed.
val print_model_human : ?filter_similar:bool ->
?me_name_trans:(model_element_name -> string) ->
Stdlib.Format.formatter -> model -> print_attrs:bool -> unit

Same as print_model but is intended to be human readable.

val print_model_json : ?me_name_trans:(model_element_name -> string) ->
?vc_line_trans:(int -> string) ->
Stdlib.Format.formatter -> model -> unit

Prints counter-example model to json format.

me_name_trans : see print_model
vc_line_trans : the transformation from the line number corresponding to the term that triggers VC before splitting VC to the name of JSON field storing counterexample information related to this term. By default, this information is stored in JSON field corresponding to this line, i.e., the transformation is string_of_int. Note that the exact line of the construct that triggers VC may not be known. This can happen if the term that triggers VC spans multiple lines and it is splitted. This transformation can be used to store the counterexample information related to this term in dedicated JSON field The format is the following: Example: "records.adb": { "84": [ { "name": "A.A", "value": "255", "kind": "other" }, { "name": "B.B", "value": "0", "kind": "other" } ] }
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

Given a source code and a counter-example model interleaves the source code with information in about the counter-example. That is, for each location in counter-example trace creates a comment in the output source code with information about values of counter-example model elements.

start_comment : the string that starts a comment
end_comment : the string that ends a comment
me_name_trans : see print_model
rel_filename : the file name of the source relative to the session
source_code : the input source code
locations : the source locations that are found in the code
val model_for_positions_and_decls : model -> positions:Loc.position list -> model

Given a model and a list of source-code positions returns model that contains only elements from the input model that are on these positions plus for every file in the model, elements that are in the positions of function declarations. Elements with other positions are filtered out.

Assumes that for each file the element on the first line of the model has position of function declaration.

Only filename and line number is used to identify positions.

class clean : object .. end

Method clean#model cleans a model from unparsed values and handles contradictory VCs ("the check fails with all inputs").

val customize_clean : #clean -> unit

Customize the class used to clean the values in the model.

type model_parser = Printer.printer_mapping -> string -> model 

Parses the input string into model elements, estabilishes a mapping between these elements and mapping from printer and builds model data structure. The model still has to be cleaned using clean.

type raw_model_parser = Printer.printer_mapping -> 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