From be6edaf05572df8a9232c6fa4101bcc6b07205a0 Mon Sep 17 00:00:00 2001
From: David Hauzar <david.hauzar@inria.fr>
Date: Wed, 22 Jul 2015 11:12:01 +0200
Subject: [PATCH] Refactoring of getting information about the term triggering
VC in counter-example.
---
src/core/printer.ml | 4 +--
src/core/printer.mli | 5 ++--
src/printer/smtv2.ml | 64 +++++++++++++++++++++++---------------------
3 files changed, 38 insertions(+), 35 deletions(-)
diff --git a/src/core/printer.ml b/src/core/printer.ml
index 8ddf974a27..fdf4d8d73e 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_line : Loc.position option;
+ vc_term : 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_line = None;
+ vc_term = None;
queried_terms = [];
}
diff --git a/src/core/printer.mli b/src/core/printer.mli
index f41850b62f..4a4728674c 100644
--- a/src/core/printer.mli
+++ b/src/core/printer.mli
@@ -28,9 +28,8 @@ 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_line : Loc.position option;
- (* The position of the term corresponding to the line in the program
- for that the VC was made *)
+ vc_term : 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
by the printer *)
diff --git a/src/printer/smtv2.ml b/src/printer/smtv2.ml
index 8ecc925883..99ef1ee027 100644
--- a/src/printer/smtv2.ml
+++ b/src/printer/smtv2.ml
@@ -80,18 +80,18 @@ let ident_printer =
let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id)
-(* Information about the line in the program for that the VC was made *)
-type vc_line_info = {
+(* Information about the term that triggers VC. *)
+type vc_term_info = {
mutable vc_inside : bool;
- (* true if the term corresponding to VC line is currently processed *)
+ (* true if the term that triggers VC is currently processed *)
mutable vc_loc : Loc.position option;
- (* the position of VC line *)
+ (* the position of the term that triggers VC *)
mutable vc_func_name : string option;
- (* the name of the function. None if VC is not generated for
- postcondition or precondition) *)
+ (* the name of the function for that VC was made. None if VC
+ is not generated for postcondition or precondition) *)
}
-let vc_line_info = { vc_inside = false; vc_loc = None; vc_func_name = None }
+let vc_term_info = { vc_inside = false; vc_loc = None; vc_func_name = None }
module TermCmp = struct
type t = term
@@ -150,7 +150,9 @@ let print_var_list info fmt vsl =
print_list space (print_typed_var info) fmt vsl
let model_label = Ident.create_label "model"
-let model_vc_line_label = Ident.create_label "model_vc"
+ (* This label identifies terms that should be in counter-example. *)
+let model_vc_term_label = Ident.create_label "model_vc"
+ (* This label identifies the term that triggers the VC. *)
let collect_model_ls info ls =
if ls.ls_args = [] && Slab.mem model_label ls.ls_name.id_label then
@@ -160,6 +162,7 @@ let collect_model_ls info ls =
(t_label ?loc:ls.ls_name.id_loc ls.ls_name.id_label t) info.info_model
let model_trace_regexp = Str.regexp "model_trace:"
+ (* The term labeled with "model_trace:name" will be in counter-example with name "name" *)
let label_starts_with regexp l =
try
@@ -200,7 +203,7 @@ let model_trace_for_postcondition ~labels =
(* no model_trace label => the term represents the return value *)
Slab.add
(Ident.create_label
- ("model_trace:" ^ (Opt.get_def "" vc_line_info.vc_func_name) ^ "@result"))
+ ("model_trace:" ^ (Opt.get_def "" vc_term_info.vc_func_name) ^ "@result"))
labels
let get_fun_name name =
@@ -211,28 +214,29 @@ let get_fun_name name =
| _ ->
""
-let check_enter_vc_line t =
- (* Check whether the term corresponding to the line of VC is entered.
- If it is entered, extract the location of VC line and if the VC is
- postcondition or precondition of a function , extract the name of
- the function.
+let check_enter_vc_term t =
+ (* Check whether the term that triggers VC is entered.
+ If it is entered, extract the location of the term and if the VC is
+ postcondition or precondition of a function, extract the name of
+ the corresponding function.
*)
- if Slab.mem model_vc_line_label t.t_label then begin
- vc_line_info.vc_inside <- true;
- vc_line_info.vc_loc <- t.t_loc;
+ if Slab.mem model_vc_term_label t.t_label then begin
+ vc_term_info.vc_inside <- true;
+ vc_term_info.vc_loc <- t.t_loc;
try
+ (* Label "model_func" => the VC is postcondition or precondition *)
(* Extract the function name from "model_func" label *)
let fun_label = get_label t.t_label (Str.regexp "model_func") in
- vc_line_info.vc_func_name <- Some (get_fun_name fun_label.lab_string);
+ vc_term_info.vc_func_name <- Some (get_fun_name fun_label.lab_string);
with Not_found ->
(* No label "model_func" => the VC is not postcondition or precondition *)
()
end
-let check_exit_vc_line t =
- (* Check whether the term corresponding to the line of VC is exited. *)
- if Slab.mem model_vc_line_label t.t_label then begin
- vc_line_info.vc_inside <- false;
+let check_exit_vc_term t =
+ (* Check whether the term triggering VC is exited. *)
+ if Slab.mem model_vc_term_label t.t_label then begin
+ vc_term_info.vc_inside <- false;
end
(** expr *)
@@ -242,7 +246,7 @@ let rec print_term info fmt t =
if Slab.mem model_label t.t_label then
info.info_model <- S.add t info.info_model;
- check_enter_vc_line t;
+ check_enter_vc_term t;
let () = match t.t_node with
| Tconst c ->
@@ -279,11 +283,11 @@ let rec print_term info fmt t =
(print_type info) t fmt tl
| None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
| [] ->
- if vc_line_info.vc_inside then begin
- match vc_line_info.vc_loc with
+ if vc_term_info.vc_inside then begin
+ match vc_term_info.vc_loc with
| None -> ()
| Some loc ->
- let labels = match vc_line_info.vc_func_name with
+ let labels = match vc_term_info.vc_func_name with
| None ->
ls.ls_name.id_label
| Some _ ->
@@ -325,7 +329,7 @@ let rec print_term info fmt t =
| Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
in
- check_exit_vc_line t;
+ check_exit_vc_term t;
and print_fmla info fmt f =
@@ -333,7 +337,7 @@ and print_fmla info fmt f =
if Slab.mem model_label f.t_label then
info.info_model <- S.add f info.info_model;
- check_enter_vc_line f;
+ check_enter_vc_term f;
let () = match f.t_node with
| Tapp ({ ls_name = id }, []) ->
@@ -404,7 +408,7 @@ and print_fmla info fmt f =
end
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f) in
- check_exit_vc_line f
+ check_exit_vc_term f
and print_boolean_branches info subject pr fmt bl =
let error () = unsupportedTerm subject
@@ -530,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_line = vc_line_info.vc_loc;
+ vc_term = vc_term_info.vc_loc;
queried_terms = model_list; }
| Plemma| Pskip -> assert false
--
GitLab