Commit 19bd2368 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'sp_counterex' into 'master'

ce: duplicate vc:written variables at appropriate locations

See merge request !66
parents 7e2595d2 ef33b483
......@@ -22,18 +22,52 @@ Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
"val" : "42" }
File if_assign.mlw:
Line 22:
the check fails with all inputs
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 25:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 27:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "-1" }
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
Line 22:
the check fails with all inputs
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
Line 25:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
Line 27:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File int.mlw:
......
......@@ -22,18 +22,52 @@ Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
"val" : "42" }
File if_assign.mlw:
Line 22:
the check fails with all inputs
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 25:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 27:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File int.mlw:
Line 16:
a, [] = {"type" : "Integer" ,
"val" : "2" }
File ref.mlw:
Line 18:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
Line 22:
the check fails with all inputs
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
Line 25:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
Line 27:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
[@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File int.mlw:
......
......@@ -349,8 +349,30 @@ let create_model_trace_attr s = create_attribute ("model_trace:" ^ s)
let is_model_trace_attr a =
Strings.has_prefix "model_trace:" a.attr_string
let is_written_attr a =
Strings.has_prefix "vc:written:" a.attr_string
let create_written_attr loc =
let f,l,b,e = Loc.get loc in
let s = Format.sprintf "vc:written:%i:%i:%i:%s" l b e f in
create_attribute s
let extract_written_loc attr =
let spl = Strings.bounded_split ':' attr.attr_string 6 in
match spl with
| "vc" :: "written" :: line :: col_st :: col_end :: file :: [] ->
begin try
let line = int_of_string line in
let col_st = int_of_string col_st in
let col_end = int_of_string col_end in
Some (Loc.user_position file line col_st col_end)
with _ -> None
end
| _ -> None
let is_counterexample_attr a =
is_model_trace_attr a || attr_equal a model_projected_attr
is_model_trace_attr a || attr_equal a model_projected_attr ||
is_written_attr a
let has_a_model_attr id =
Sattr.exists is_counterexample_attr id.id_attrs
......
......@@ -180,6 +180,21 @@ val relevant_for_counterexample: ident -> bool
counterexamples generation.
*)
val create_written_attr: Loc.position -> attribute
(** The vc_written attribute is built during VC generation: it is used to
track the location of the creation of variables. Those variables can have
several creation locations with SP algorithm. These attribute-locations are
used by counterexamples.
The form is the following:
"vc:written:line:start_column:end_column:file_name"
file_name is at the end for easier parsing (file_name can contain ":")
*)
val extract_written_loc: attribute -> Loc.position option
(** Extract the location inside vc_written attribute. [None] if the attribute is
ill-formed.
*)
val remove_model_attrs : attrs:Sattr.t -> Sattr.t
(** Remove the counter-example attributes from an attribute set *)
......
......@@ -862,7 +862,17 @@ let build_model_rec (raw_model: model_element list) (term_map: Term.term Mstr.t)
me_location = t.t_loc;
me_term = Some t;
} in
add_to_model model model_element
let model = add_to_model model model_element in
(* Here we create the same element for all its possible locations (given
by attribute vc:written).
*)
Sattr.fold (fun attr model ->
let loc = Ident.extract_written_loc attr in
if loc = None then
model
else
add_to_model model {model_element with me_location = loc}
) attrs model
)
with Not_found -> model)
model
......
......@@ -126,7 +126,8 @@ val create_model_element :
@param location : source-code location of the element
@param term : why term corresponding to the element *)
@param term : why term corresponding to the element
*)
(*
***************************************************************
......
......@@ -1213,12 +1213,8 @@ let ht_written = Hvs.create 17
let fresh_loc_attrs = Loc.dummy_position, Sattr.empty
let wrt_mk_loc_attr = function
| Some loc ->
let f,l,b,e = Loc.get loc in
let s = Format.sprintf "vc:written:%i:%i:%i:%s" l b e f in
Some (loc, create_attribute s)
| None -> None
let wrt_mk_loc_attr loc =
Opt.map (fun loc -> loc, create_written_attr loc) loc
let wrt_add_loc_attr v = function
| Some (loc,attr) ->
......@@ -1311,7 +1307,7 @@ let rec sp_expr kn k rdm dst = match k with
let new_written = ref [] in
let mk_written v =
let n = clone_pv None v in
(* if relevant_for_counterexample v.pv_vs.vs_name then *) begin
if relevant_for_counterexample v.pv_vs.vs_name then begin
Hvs.add ht_written n fresh_loc_attrs;
new_written := n :: !new_written
end;
......
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