Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 442e9a59 authored by MARCHE Claude's avatar MARCHE Claude

traceability: locations with special tokens

parent 9ceb1577
......@@ -67,44 +67,21 @@ let create_ident name origin labels = {
id_tag = Hashweak.dummy_tag;
}
let file_regexp = Str.regexp "file:\\(.*\\)"
let line_regexp = Str.regexp "line:\\([0-9]+\\)"
let begin_regexp = Str.regexp "begin:\\([0-9]+\\)"
let end_regexp = Str.regexp "end:\\([0-9]+\\)"
let id_fresh ?(labels = []) nm = create_ident nm Fresh labels
let id_user ?(labels = []) nm loc =
(*
let (f,li,b,e) = Loc.extract loc in
let f = ref f in
let li = ref li in
let b = ref b in
let e = ref e in
let l = List.fold_left
(fun acc ((s,_) as lab) ->
if Str.string_match file_regexp s 0 then
(f := Str.matched_group 1 s; acc)
else
if Str.string_match line_regexp s 0 then
(li := int_of_string (Str.matched_group 1 s); acc)
else
if Str.string_match begin_regexp s 0 then
(b := int_of_string (Str.matched_group 1 s); acc)
else
if Str.string_match end_regexp s 0 then
(e := int_of_string (Str.matched_group 1 s); acc)
else lab :: acc)
let new_loc = ref loc in
let new_labels = List.fold_left
(fun acc ((s,l) as lab) ->
match l with
| None -> lab :: acc
| Some loc ->
new_loc := loc;
match s with
| "" -> acc
| _ -> lab :: acc)
[] labels
in
let loc =
({Lexing.pos_fname = !f; Lexing.pos_lnum = !li;
Lexing.pos_bol = 0; Lexing.pos_cnum = !b},
{Lexing.pos_fname = !f; Lexing.pos_lnum = !li;
Lexing.pos_bol = 0; Lexing.pos_cnum = !e})
in
*)
let l = labels in
create_ident nm (User loc) l
create_ident nm (User !new_loc) new_labels
let id_derive ?(labels = []) nm id = create_ident nm (Derived id) labels
......
......@@ -330,8 +330,8 @@ and wp_desc env e q = match e.expr_desc with
| Some i ->
wp_and wfr
(wp_and ~sym:true
(f_label_add (label "LoopInvInit") i)
(f_label_add (label "LoopInvPres")
(f_label_add (label "expl:Loop invariant init") i)
(f_label_add (label "expl:Loop invariant preservation")
(quantify env e.expr_effect (wp_implies i we))))
in
w
......@@ -418,10 +418,10 @@ and wp_desc env e q = match e.expr_desc with
| Eassert (Ptree.Aassert, f) ->
let (_, q), _ = q in
wp_and (f_label_add (label "Assert") f) q
wp_and (f_label_add (label "expl:assertion") f) q
| Eassert (Ptree.Acheck, f) ->
let (_, q), _ = q in
wp_and ~sym:true (f_label_add (label "Check") f) q
wp_and ~sym:true (f_label_add (label "expl:check") f) q
| Eassert (Ptree.Aassume, f) ->
let (_, q), _ = q in
wp_implies f q
......@@ -431,7 +431,7 @@ and wp_desc env e q = match e.expr_desc with
| Eany c ->
(* TODO: propagate call labels into c.c_post *)
let w = opaque_wp env c.c_effect c.c_post q in
let p = f_label_add (label ~loc:e.expr_loc "Pre") c.c_pre in
let p = f_label_add (label ~loc:e.expr_loc "expl:precondition") c.c_pre in
wp_and p w
and wp_triple env (p, e, q) =
......
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