Storing counter-example model elements related to the term that

triggers VC in Model_parser.model and printing them.

src/core/model_parser.ml

@@ -144,10 +144,20 @@ module IntMap = Map.Make(struct type t  = int let compare = compare end)
 module StringMap = Map.Make(String)
 
 type model_file = model_element list IntMap.t
-type model = model_file StringMap.t
+type model_files = model_file StringMap.t
+type model = {
+  vc_term_loc : Loc.position option;
+  model_files : model_files;
+}
 
 let empty_model = StringMap.empty
 let empty_model_file = IntMap.empty
+let is_model_empty model =
+  model.model_files = empty_model
+let default_model = {
+  vc_term_loc = None;
+  model_files = empty_model;
+}
 
 type model_parser =  string -> Printer.printer_mapping -> model
 
@@ -184,7 +194,7 @@ let print_model
     ?(me_name_trans = why_name_trans)
     fmt
     model =
-  StringMap.iter (print_model_file fmt me_name_trans) model
+  StringMap.iter (print_model_file fmt me_name_trans) model.model_files
 
 let model_to_string
     ?(me_name_trans = why_name_trans)
@@ -204,6 +214,19 @@ let get_elements model_file line_number =
   with Not_found ->
     []
 
+let print_model_vc_term
+    ?(me_name_trans = why_name_trans)
+    ?(sep = "\n")
+    fmt
+    model =
+  match model.vc_term_loc with
+  | None -> ()
+  | Some pos ->
+    let (filename, line_number, _, _) = Loc.get pos in
+    let model_file = get_model_file model.model_files filename in
+    let model_elements = get_elements model_file line_number in
+    print_model_elements ~sep me_name_trans fmt model_elements
+
 let get_padding line =
   try
     let r = Str.regexp " *" in
@@ -240,7 +263,7 @@ let interleave_with_source
     ~filename
     ~source_code =
   try
-    let model_file = StringMap.find  filename model in
+    let model_file = StringMap.find  filename model.model_files in
     let lines = Str.split (Str.regexp "^") source_code in
     let (source_code, _) = List.fold_left
       (interleave_line
@@ -290,7 +313,7 @@ let print_model_json
     (fun s -> s)
     (print_model_elements_on_lines_json me_name_to_str)
     fmt
-    (StringMap.bindings model)
+    (StringMap.bindings model.model_files)
 
 let model_to_string_json
     ?(me_name_trans = why_name_trans)
@@ -359,9 +382,12 @@ match raw_model with
       terms_tail
       model
 
-
 let build_model raw_model printer_mapping =
-  build_model_rec raw_model printer_mapping.queried_terms empty_model
+  let model_files = build_model_rec raw_model printer_mapping.queried_terms empty_model in
+  {
+    vc_term_loc = printer_mapping.Printer.vc_term_loc;
+    model_files = model_files;
+  }
 
 
 (*
@@ -399,11 +425,13 @@ let add_first_model_line filename model_file model =
 let model_for_positions_and_decls model ~positions =
   (* Start with empty model and add locations from model that
      are in locations *)
-  let model_filtered = List.fold_left (add_loc model) empty_model positions in
+  let model_filtered = List.fold_left (add_loc model.model_files) empty_model positions in
   (* For each file add mapping corresponding to the first line of the
      counter-example from model to model_filtered.
      This corresponds to function declarations *)
-  StringMap.fold add_first_model_line model model_filtered
+  let model_filtered = StringMap.fold add_first_model_line model.model_files model_filtered in
+  { vc_term_loc = model.vc_term_loc;
+    model_files = model_filtered }
 
 
 (*

src/core/model_parser.mli

@@ -101,7 +101,8 @@ val create_model_element :
 *)
 type model
 
-val empty_model : model
+val is_model_empty : model -> bool
+val default_model : model
 
 (*
 ***************************************************************
@@ -129,6 +130,20 @@ val model_to_string :
   string
 (** See print_model  *)
 
+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.
+*)
+
 val print_model_json :
   ?me_name_trans:((string * model_element_type) -> string) ->
   Format.formatter ->

src/core/printer.ml

@@ -30,7 +30,7 @@ type 'a pp = Pp.formatter -> 'a -> unit
 
 type printer_mapping = {
   lsymbol_m     : string -> Term.lsymbol;
-  vc_term       : Loc.position option;
+  vc_term_loc   : Loc.position option;
   queried_terms : Term.term list;
 }
 
@@ -53,7 +53,7 @@ exception UnknownPrinter of string
 
 let get_default_printer_mapping = {
   lsymbol_m = (function _ -> raise Not_found);
-  vc_term = None;
+  vc_term_loc = None;
   queried_terms = [];
 }
 

src/core/printer.mli

@@ -28,7 +28,7 @@ type 'a pp = Format.formatter -> 'a -> unit
 in the output of the printer to elements of AST in its input. *)
 type printer_mapping = {
   lsymbol_m     : string -> Term.lsymbol;
-  vc_term       : Loc.position option;
+  vc_term_loc   : Loc.position option;
   (* The position of the term that triggers the VC *)
   queried_terms : Term.term list;
   (* The list of terms that were queried for the counter-example

src/driver/call_provers.ml

@@ -135,7 +135,7 @@ let print_steps fmt s =
 let print_prover_result fmt
   {pr_answer=ans; pr_status=status; pr_output=out; pr_time=t; pr_steps=s; pr_model=m} =
   fprintf fmt "%a (%.2fs%a)" print_prover_answer ans t print_steps s;
-  if m <> Model_parser.empty_model then begin
+  if Model_parser.is_model_empty m then begin
     fprintf fmt "\nCounter-example model:";
     Model_parser.print_model fmt m
   end;

src/ide/gmain.ml

@@ -642,7 +642,7 @@ let update_tabs a =
       begin
         match a.S.proof_state with
 	  | S.Done r ->
-	    if r.Call_provers.pr_model <> Model_parser.empty_model then begin
+	    if Model_parser.is_model_empty r.Call_provers.pr_model then begin
 	      Model_parser.interleave_with_source
 		r.Call_provers.pr_model
 		~filename:!current_file

src/printer/smtv2.ml

@@ -534,7 +534,7 @@ let print_prop_decl cntexample args info fmt k pr f = match k with
       print_info_model cntexample fmt model_list info;
 
       args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
-				vc_term = vc_term_info.vc_loc;
+				vc_term_loc = vc_term_info.vc_loc;
 				queried_terms = model_list; }
   | Plemma| Pskip -> assert false
 

src/session/session.ml

@@ -1194,7 +1194,7 @@ let load_result r =
           Call_provers.pr_output = "";
           Call_provers.pr_status = Unix.WEXITED 0;
 	  Call_provers.pr_steps = steps;
-	  Call_provers.pr_model = Model_parser.empty_model
+	  Call_provers.pr_model = Model_parser.default_model
         }
     | "undone" -> Interrupted
     | "unedited" -> Unedited

src/session/session_scheduler.ml

@@ -294,7 +294,7 @@ let schedule_edition t command filename callback =
       Call_provers.prp_regexps = [];
       Call_provers.prp_timeregexps = [];
       Call_provers.prp_stepregexps = [];
-      Call_provers.prp_model_parser = fun _ _ -> Model_parser.empty_model
+      Call_provers.prp_model_parser = fun _ _ -> Model_parser.default_model
     } in
   let precall =
     Call_provers.call_on_file ~command ~res_parser ~redirect:false filename ~printer_mapping:Printer.get_default_printer_mapping in