model_parser.mli 8.75 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
 | Bitvector of int
21
 | Unparsed of string
22
and  arr_index = {
23
  arr_index_key : model_value;
24 25 26 27 28 29 30
  arr_index_value : model_value;
}
and model_array = {
  arr_others  : model_value;
  arr_indices : arr_index list;
}

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

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

44 45 46 47 48 49 50 51
    @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

52 53

(*
54
***************************************************************
55 56 57
**  Model elements
***************************************************************
*)
58

59
type model_element_kind =
60 61 62
| Result
  (* Result of a function call (if the counter-example is for postcondition)  *)
| Old
63 64 65 66
  (* Old value of function argument (if the counter-example is for postcondition) *)
| Error_message
  (* The model element represents error message, not source-code element.
     The error message is saved in the name of the model element.*)
67 68
| Other

69 70 71 72 73 74 75
(** Information about the name of the model element *)
type model_element_name = {
  men_name   : string;
    (** The name of the source-code element.  *)
  men_kind   : model_element_kind;
    (** The kind of model element. *)
}
76

77 78
(** Counter-example model elements. Each element represents
    a counter-example for a single source-code element.*)
79
type model_element = {
80 81
  me_name     : model_element_name;
    (** Information about the name of the model element  *)
82 83 84 85
  me_value    : model_value;
    (** Counter-example value for the element. *)
  me_location : Loc.position option;
    (** Source-code location of the element. *)
86 87
  me_term     : Term.term option;
    (** Why term corresponding to the element.  *)
88 89
}

90 91 92 93
val create_model_element :
  name     : string ->
  value    : model_value ->
  ?location : Loc.position ->
94 95
  ?term     : Term.term ->
  unit ->
96
  model_element
97
(** Creates a counter-example model element.
98 99 100 101
    @param name : the name of the source-code element

    @param value  : counter-example value for the element

102 103
    @param location : source-code location of the element

104
    @param term : why term corresponding to the element *)
105

106
(*
107
***************************************************************
108 109
**  Model definitions
***************************************************************
110 111
*)
type model
112

113 114
val is_model_empty : model -> bool
val default_model : model
115 116

(*
117
***************************************************************
118 119 120
**  Quering the model
***************************************************************
*)
121

122
val print_model :
123
  ?me_name_trans:(model_element_name -> string) ->
124
  Format.formatter ->
125
  model ->
126 127 128 129
  unit
(** Prints the counter-example model

    @param me_name_trans the transformation of the model elements
130 131
      names. The input is information about model element name. The
      output is the name of the model element that should be displayed.
132 133 134 135
    @param model the counter-example model to print
*)

val model_to_string :
136
  ?me_name_trans:(model_element_name -> string) ->
137 138 139
  model ->
  string
(** See print_model  *)
140

141
val print_model_vc_term :
142
  ?me_name_trans: (model_element_name -> string) ->
143 144 145 146 147 148 149 150 151 152 153 154
  ?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.
*)

155
val model_vc_term_to_string :
156
  ?me_name_trans: (model_element_name -> string) ->
157 158 159 160 161 162 163 164
  ?sep: string ->
  model ->
  string
(** Gets string with counter-example model elements related to term that
    triggers VC.
    See print_model_vc_term
*)

165
val print_model_json :
166
  ?me_name_trans:(model_element_name -> string) ->
167
  Format.formatter ->
168
  model ->
169 170
  unit
(** Prints counter-example model to json format.
171

172 173 174 175 176 177 178 179 180 181 182 183
    The format is the following:
    - counterexample is JSON object with fields indexed by names of files
      storing values of counterexample_file
    - counterexample_file is JSON object with fields indexed by line numbers
      storing values of counterexample_line
    - counterexample_line is JSON array (ordered list) with elements
      corresponding to counterexample_element
    - counterexample_element is JSON object with following fields
      - "name": name of counterexample element
      - "value": value of counterexample element
      - "kind": kind of counterexample element:
        - "result": Result of a function call (if the counter-example is for postcondition)
184
        - "old": Old value of function argument (if the counter-example is for postcondition)
185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206
        - "error_message": The model element represents error message, not source-code element.
            The error message is saved in the name of the model element
        - "other"

    Example:
    {
      "records.adb": {
          "84": [
            {
              "name": "A.A",
              "value": "255",
              "kind": "other"
            },
            {
              "name": "B.B",
              "value": "0",
              "kind": "other"
            }
          ]
      }
    }

207 208 209
    @param me_name_trans see print_model
    @model the counter-example model to print.
*)
210

211
val model_to_string_json :
212
  ?me_name_trans:(model_element_name -> string) ->
213 214 215
  model ->
  string
(** See print_model_json *)
216

217
val interleave_with_source :
218 219
  ?start_comment:string ->
  ?end_comment:string ->
220
  ?me_name_trans:(model_element_name -> string) ->
221
  model ->
222 223
  filename:string ->
  source_code:string ->
224
  string
225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240
(** 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
*)
241 242

(*
243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262
***************************************************************
**  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.
*)

(*
***************************************************************
263 264 265 266
** Registering model parser
***************************************************************
*)
type model_parser =  string -> Printer.printer_mapping -> model
267 268
(** Parses the input string into model elements, estabilishes
    a mapping between these elements and mapping from printer
269 270
    and builds model data structure.
*)
271

272 273
type raw_model_parser =  string -> model_element list
(** Parses the input string into model elements. *)
274

275
val register_model_parser : desc:Pp.formatted -> string -> raw_model_parser -> unit
276 277 278 279

val lookup_model_parser : string -> model_parser

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