model_parser.mli 7.44 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12
(*
13
***************************************************************
14 15 16
**  Counter-example model values
****************************************************************
*)
17 18 19
type model_value =
 | Integer of string
 | Array of model_array
20
 | Unparsed of string
21 22 23 24 25 26 27 28 29
and  arr_index = {
  arr_index_key : int;
  arr_index_value : model_value;
}
and model_array = {
  arr_others  : model_value;
  arr_indices : arr_index list;
}

30 31
val array_create_constant :
  value : model_value ->
32 33 34
  model_array
(** Creates constant array with all indices equal to the parameter value. *)

35 36 37 38
val array_add_element :
  array : model_array ->
  index : model_value ->
  value : model_value ->
39
  model_array
40
(** Adds an element to the array.
41
    @param array : the array to that the element will be added
42

43 44 45 46 47 48 49 50
    @param index : the index on which the element will be added.
    Note that the index must be of value model_value.Integer

    @param value : the value of the element to be added
*)

val print_model_value : Format.formatter -> model_value -> unit

51 52

(*
53
***************************************************************
54 55 56
**  Model elements
***************************************************************
*)
57 58 59 60 61 62 63 64 65

type model_element_type =
| Result
  (* Result of a function call (if the counter-example is for postcondition)  *)
| Old
  (* Old value of function argument (if the counter-example is for postcondition)  *)
| Other


66 67
(** Counter-example model elements. Each element represents
    a counter-example for a single source-code element.*)
68
type model_element = {
69
  me_name     : string;
70
    (** The name of the source-code element.  *)
71 72
  me_type     : model_element_type;
    (** The type of model element. *)
73 74 75 76
  me_value    : model_value;
    (** Counter-example value for the element. *)
  me_location : Loc.position option;
    (** Source-code location of the element. *)
77 78
  me_term     : Term.term option;
    (** Why term corresponding to the element.  *)
79 80 81 82
  me_text_info: bool;
    (** True if the model element represents just textual
        information and not source-code element.
        In this case, just me_name is printed, not its value.*)
83 84
}

85 86 87 88
val create_model_element :
  name     : string ->
  value    : model_value ->
  ?location : Loc.position ->
89 90
  ?term     : Term.term ->
  unit ->
91
  model_element
92
(** Creates a counter-example model element.
93 94 95 96
    @param name : the name of the source-code element

    @param value  : counter-example value for the element

97 98
    @param location : source-code location of the element

99
    @param term : why term corresponding to the element *)
100

101
(*
102
***************************************************************
103 104
**  Model definitions
***************************************************************
105 106
*)
type model
107

108 109
val is_model_empty : model -> bool
val default_model : model
110 111

(*
112
***************************************************************
113 114 115
**  Quering the model
***************************************************************
*)
116

117 118 119
val print_model :
  ?me_name_trans:((string * model_element_type) -> string) ->
  Format.formatter ->
120
  model ->
121 122 123 124 125 126 127 128 129 130 131 132 133 134 135
  unit
(** Prints the counter-example model

    @param me_name_trans the transformation of the model elements
      names. The input is a pair consisting of the name of model
      element and type of the model element. The output is the
      name of the model element that should be displayed.
    @param model the counter-example model to print
*)

val model_to_string :
  ?me_name_trans:((string * model_element_type) -> string) ->
  model ->
  string
(** See print_model  *)
136

137 138 139 140 141 142 143 144 145 146 147 148 149 150
val print_model_vc_term :
  ?me_name_trans: ((string * model_element_type) -> string) ->
  ?sep: string ->
  Format.formatter ->
  model ->
  unit
(** Prints counter-example model elements related to term that
    triggers VC.

    @param sep separator of counter-example model elements
    @param me_name_trans see print_model
    @model the counter-example model.
*)

151 152 153 154 155 156 157 158 159 160
val model_vc_term_to_string :
  ?me_name_trans: ((string * model_element_type) -> string) ->
  ?sep: string ->
  model ->
  string
(** Gets string with counter-example model elements related to term that
    triggers VC.
    See print_model_vc_term
*)

161 162 163
val print_model_json :
  ?me_name_trans:((string * model_element_type) -> string) ->
  Format.formatter ->
164
  model ->
165 166
  unit
(** Prints counter-example model to json format.
167

168 169 170
    @param me_name_trans see print_model
    @model the counter-example model to print.
*)
171

172 173 174 175 176
val model_to_string_json :
  ?me_name_trans:((string * model_element_type) -> string) ->
  model ->
  string
(** See print_model_json *)
177

178
val interleave_with_source :
179 180
  ?start_comment:string ->
  ?end_comment:string ->
181
  ?me_name_trans:((string * model_element_type) -> string) ->
182
  model ->
183 184
  filename:string ->
  source_code:string ->
185
  string
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201
(** 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.

    @param start_comment the string that starts a comment
    @param end_comment the string that ends a comment
    @param me_name_trans see print_model
    @param model counter-example model
    @param filename the file name of the source
    @param source_code the input source code

    @return the source code with added comments with information
    about counter-example model
*)
202 203

(*
204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223
***************************************************************
**  Filtering the model
***************************************************************
*)
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.
*)

(*
***************************************************************
224 225 226 227
** Registering model parser
***************************************************************
*)
type model_parser =  string -> Printer.printer_mapping -> model
228 229
(** Parses the input string into model elements, estabilishes
    a mapping between these elements and mapping from printer
230 231
    and builds model data structure.
*)
232

233 234
type raw_model_parser =  string -> model_element list
(** Parses the input string into model elements. *)
235

236
val register_model_parser : desc:Pp.formatted -> string -> raw_model_parser -> unit
237 238 239 240

val lookup_model_parser : string -> model_parser

val list_model_parsers : unit -> (string * Pp.formatted) list