diff --git a/src/core/model_parser.ml b/src/core/model_parser.ml index 1ab8c0624d71fceb07c57e88138f3e1f144d4798..e950006f1dd3943ccb41c38594abec8b46eedaa9 100644 --- a/src/core/model_parser.ml +++ b/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 } (* diff --git a/src/core/model_parser.mli b/src/core/model_parser.mli index 93a5785d0bf34e16250626a1988478f1f3995d09..becedb3615a897e6aa866be13caddddf716c066c 100644 --- a/src/core/model_parser.mli +++ b/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 -> diff --git a/src/core/printer.ml b/src/core/printer.ml index fdf4d8d73ef86fe15e9705c9e4e063732b4fae32..9e5355128533a977f605f0c6cb6893fadde9c2d7 100644 --- a/src/core/printer.ml +++ b/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 = []; } diff --git a/src/core/printer.mli b/src/core/printer.mli index 4a4728674c9eab9e9e8727b77fc06bc7a1b24fd5..e29a2a223a5948836eb6002b5504bd844bfaaa38 100644 --- a/src/core/printer.mli +++ b/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 diff --git a/src/driver/call_provers.ml b/src/driver/call_provers.ml index 8979030b4d0446b929398a84ae64d59d5c0f253c..78924af69c865c5dc3e48949705de0c1a21f76f5 100644 --- a/src/driver/call_provers.ml +++ b/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; diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml index 005ad50f3cdf04540678a269a35d79cf228a2d7f..8a593e6efa960233bf939593222c4b1b0973ecb9 100644 --- a/src/ide/gmain.ml +++ b/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 diff --git a/src/printer/smtv2.ml b/src/printer/smtv2.ml index 99ef1ee027d1af17fde6bdd7ae143b5b44bbfb29..ba1b50f5df044251dd820690f0a685ecc75ecaf4 100644 --- a/src/printer/smtv2.ml +++ b/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 diff --git a/src/session/session.ml b/src/session/session.ml index 13ab8fb2becbb77931e5347688c082c9271b49a0..066390021ca3f6b1a38da344ec71a6bcfd398e4d 100644 --- a/src/session/session.ml +++ b/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 diff --git a/src/session/session_scheduler.ml b/src/session/session_scheduler.ml index d2a652787a84c27efea5731b7c0c1eb43109dd15..e3f7b49cbf3610aa91fa8d1f24ae62b60ae592c0 100644 --- a/src/session/session_scheduler.ml +++ b/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