Commit 1038e22b authored by MARCHE Claude's avatar MARCHE Claude

disabled useless code for counterexamples

parent ed44cafa
......@@ -19,7 +19,9 @@ x = {"type" : "Integer" ,
bench/ce/int.mlw T newgoal : Unknown (other)
Counter-example model:File int.mlw:
Line 14:
x2 = {"type" : "Integer" , "val" : "1" }
X = {"type" : "Integer" , "val" : "1" }
x2 = {"type" : "Integer" ,
"val" : "1" }
x3 = {"type" : "Integer" ,
"val" : "1" }
x4 = {"type" : "Integer" ,
......@@ -54,7 +56,9 @@ x = {"type" : "Integer" ,
bench/ce/int.mlw T newgoal : Unknown (other)
Counter-example model:File int.mlw:
Line 14:
x2 = {"type" : "Integer" , "val" : "1" }
X = {"type" : "Integer" , "val" : "1" }
x2 = {"type" : "Integer" ,
"val" : "1" }
x3 = {"type" : "Integer" ,
"val" : "1" }
x4 = {"type" : "Integer" ,
......
......@@ -19,7 +19,9 @@ x = {"type" : "Integer" ,
bench/ce/int.mlw T newgoal : Unknown (other)
Counter-example model:File int.mlw:
Line 14:
x2 = {"type" : "Integer" , "val" : "1" }
X = {"type" : "Integer" , "val" : "1" }
x2 = {"type" : "Integer" ,
"val" : "1" }
x3 = {"type" : "Integer" ,
"val" : "1" }
x4 = {"type" : "Integer" ,
......@@ -54,7 +56,9 @@ x = {"type" : "Integer" ,
bench/ce/int.mlw T newgoal : Unknown (other)
Counter-example model:File int.mlw:
Line 14:
x2 = {"type" : "Integer" , "val" : "1" }
X = {"type" : "Integer" , "val" : "1" }
x2 = {"type" : "Integer" ,
"val" : "1" }
x3 = {"type" : "Integer" ,
"val" : "1" }
x4 = {"type" : "Integer" ,
......
......@@ -45,9 +45,9 @@ x.g = {"type" : "Boolean" ,
bench/ce/records.mlw M WP_parameter test_record_match_eval_test5 : Unknown (other)
Counter-example model:File ref.mlw:
Line 18:
old re.my_field_f = {"type" : "Integer" ,
re.my_field_f = {"type" : "Integer" ,
"val" : "5" }
old re.g = {"type" : "Boolean" ,
re.g = {"type" : "Boolean" ,
"val" : false }
x.my_field_f = {"type" : "Integer" ,
"val" : "6" }
......
......@@ -45,9 +45,9 @@ x.g = {"type" : "Boolean" ,
bench/ce/records.mlw M WP_parameter test_record_match_eval_test5 : Unknown (other)
Counter-example model:File ref.mlw:
Line 18:
old re.my_field_f = {"type" : "Integer" ,
re.my_field_f = {"type" : "Integer" ,
"val" : "3" }
old re.g = {"type" : "Boolean" ,
re.g = {"type" : "Boolean" ,
"val" : false }
x.my_field_f = {"type" : "Integer" ,
"val" : "6" }
......
......@@ -174,28 +174,32 @@ let rec print_term info fmt t =
Number.print number_format fmt c
| Tvar { vs_name = id } ->
print_ident info fmt id
| Tapp (ls, tl) -> begin
(match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments s (print_term info) fmt tl
| None ->
| Tapp (ls, tl) ->
begin
match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments s (print_term info) fmt tl
| None ->
begin
if (tl = []) then
begin
let vc_term_info = info.info_vc_term in
if vc_term_info.vc_inside then begin
match vc_term_info.vc_loc with
| None -> ()
| Some loc ->
let labels = match vc_term_info.vc_func_name with
| None ->
ls.ls_name.id_label
| Some _ ->
model_trace_for_postcondition ~labels:ls.ls_name.id_label info.info_vc_term in
let _t_check_pos = t_label ~loc labels t in
(* TODO: temporarily disable collecting variables inside the term triggering VC *)
(*info.info_model <- add_model_element t_check_pos info.info_model;*)
()
end
if vc_term_info.vc_inside then
begin
match vc_term_info.vc_loc with
| None -> ()
| Some loc ->
let labels = (*match vc_term_info.vc_func_name with
| None ->*)
ls.ls_name.id_label
(*| Some _ ->
model_trace_for_postcondition ~labels:ls.ls_name.id_label info.info_vc_term
*)
in
let _t_check_pos = t_label ~loc labels t in
(* TODO: temporarily disable collecting variables inside the term triggering VC *)
(*info.info_model <- add_model_element t_check_pos info.info_model;*)
()
end
end;
end;
if (Mls.mem ls info.info_csm) then
......@@ -218,7 +222,7 @@ let rec print_term info fmt t =
fprintf fmt "(%a%a : %a)" (print_ident info) ls.ls_name
(print_tapp info) tl (print_type info) (t_type t)
end
) end
end
| Tlet _ -> unsupportedTerm t
"alt-ergo : you must eliminate let in term"
| Tif _ -> unsupportedTerm t
......
......@@ -77,6 +77,7 @@ let add_model_element (el: term) info_model =
let info_model = S.remove el info_model in
S.add el info_model
(*
let add_old lab_str =
try
let pos = Str.search_forward (Str.regexp "@") lab_str 0 in
......@@ -109,6 +110,7 @@ let model_trace_for_postcondition ~labels (info: vc_term_info) =
(Ident.create_model_trace_label
((Opt.get_def "" info.vc_func_name) ^ "@result"))
labels
*)
let get_fun_name name =
let splitted = Strings.bounded_split ':' name 2 in
......
......@@ -34,7 +34,9 @@ module S : Set.S with type elt = term and type t = Set.Make(TermCmp).t
val add_model_element: Term.term -> S.t -> S.t
(*
val model_trace_for_postcondition: labels: unit Ident.Mlab.t -> vc_term_info -> unit Ident.Mlab.t
*)
val check_enter_vc_term: Term.term -> bool -> vc_term_info -> unit
......
......@@ -263,11 +263,13 @@ let rec print_term info fmt t =
match vc_term_info.vc_loc with
| None -> ()
| Some loc ->
let labels = match vc_term_info.vc_func_name with
| None ->
let labels = (* match vc_term_info.vc_func_name with
| None -> *)
ls.ls_name.id_label
| Some _ ->
model_trace_for_postcondition ~labels:ls.ls_name.id_label info.info_vc_term in
(* | Some _ ->
model_trace_for_postcondition ~labels:ls.ls_name.id_label info.info_vc_term
*)
in
let _t_check_pos = t_label ~loc labels t in
(* TODO: temporarily disable collecting variables inside the term triggering VC *)
(*info.info_model <- add_model_element t_check_pos info.info_model;*)
......
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