Commit 924c3f18 authored by David Hauzar's avatar David Hauzar
Browse files

Store counterexample information related to VC in a special index.

Since the exact line of the construct that triggers VC may not be
known, the possibility to map the counterexample information related
to this construct to dedicated index instead of mapping it to line
number was added.

Note that the line of the construct that triggers VC is guaranteed to
be known only if  this construct does not span to multiple lines or if
the VC is not split.
parent d6f70069
......@@ -64,14 +64,16 @@ let rec print_indices fmt indices =
match indices with
| [] -> ()
| index::tail ->
fprintf fmt "; %a -> " print_model_value index.arr_index_key;
fprintf fmt "%a => " print_model_value index.arr_index_key;
print_model_value fmt index.arr_index_value;
fprintf fmt ", ";
print_indices fmt tail
print_array fmt arr =
fprintf fmt "(others => ";
print_model_value fmt arr.arr_others;
fprintf fmt "(";
print_indices fmt arr.arr_indices;
fprintf fmt "others => ";
print_model_value fmt arr.arr_others;
fprintf fmt ")"
print_model_value_sanit sanit_print fmt value =
......@@ -326,29 +328,47 @@ let print_model_elements_json me_name_to_str fmt model_elements =
let print_model_elements_on_lines_json me_name_to_str fmt model_file =
let print_model_elements_on_lines_json model me_name_to_str vc_line_trans fmt
(file_name, model_file) =
(fun i -> string_of_int i)
(fun i ->
match model.vc_term_loc with
| None ->
string_of_int i
| Some pos ->
let (vc_file_name, line, _, _) = Loc.get pos in
if file_name = vc_file_name && i = line then
vc_line_trans i
string_of_int i
(print_model_elements_json me_name_to_str)
(IntMap.bindings model_file)
let print_model_json
?(me_name_trans = why_name_trans)
?(vc_line_trans = (fun i -> string_of_int i))
model =
let me_name_to_str = fun me ->
me_name_trans me.me_name in
let model_files_bindings = List.fold_left
(fun bindings (file_name, model_file) ->
List.append bindings [(file_name, (file_name, model_file))])
(StringMap.bindings model.model_files) in
(fun s -> s)
(print_model_elements_on_lines_json me_name_to_str)
(print_model_elements_on_lines_json model me_name_to_str vc_line_trans)
(StringMap.bindings model.model_files)
let model_to_string_json
?(me_name_trans = why_name_trans)
?(vc_line_trans = (fun i -> string_of_int i))
model =
print_model_json str_formatter ~me_name_trans model;
print_model_json str_formatter ~me_name_trans ~vc_line_trans model;
flush_str_formatter ()
......@@ -164,11 +164,22 @@ val model_vc_term_to_string :
val print_model_json :
?me_name_trans:(model_element_name -> string) ->
?vc_line_trans:(int -> string) ->
Format.formatter ->
model ->
(** Prints counter-example model to json format.
@param me_name_trans see print_model
@param vc_line_trans the transformation of the line corresponding to the term
that triggers VC to the name of JSON field storing counterexample information
related to this term.
It can be used to store the counterexample information related to this term
in dedicated JSON field in cases where the exact line of this term cannot be
computed - this can happen when VC is splitted.
By default, string_of_int
@model the counter-example model to print.
The format is the following:
- counterexample is JSON object with fields indexed by names of files
storing values of counterexample_file
......@@ -203,13 +214,11 @@ val print_model_json :
@param me_name_trans see print_model
@model the counter-example model to print.
val model_to_string_json :
?me_name_trans:(model_element_name -> string) ->
?vc_line_trans:(int -> string) ->
model ->
(** See print_model_json *)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment