Commit e6b7c454 authored by Allan Blanchard's avatar Allan Blanchard

[parser] Adds warning when dropping froms

parent f8f9cd0f
......@@ -120,10 +120,10 @@
let compare_pair (curb,_) (newb,_) = is_same_lexpr curb newb in
(* NB: the following has an horrible complexity, but the order of
clauses in the input is preserved. *)
let concat_one acc (l, newf) =
let (_, newf) as p = filter_from l newf in
let concat_one acc (newloc, newf) =
let (newloc, newf) as p = filter_from newloc newf in
try
let (_,curf) = List.find (compare_pair p) acc
let (curloc,curf) = List.find (compare_pair p) acc
in
match (curf, newf) with
| _,FromAny ->
......@@ -142,8 +142,21 @@
let incl l lin =
List.(for_all (fun e -> exists (is_same_lexpr e) lin) l)
in
if incl curl newl then acc
else if incl newl curl then Extlib.replace compare_pair p acc
let drop d k =
Kernel.warning ~current:false
"Drop '%a' \\from at %a for more precise one at %a"
Logic_print.print_lexpr curloc
Cil_datatype.Location.pretty d.lexpr_loc
Cil_datatype.Location.pretty k.lexpr_loc
in
if incl curl newl then begin
if not (incl newl curl) then drop newloc curloc;
acc
end
else if incl newl curl then begin
drop curloc newloc;
Extlib.replace compare_pair p acc
end
else acc @ [p]
with Not_found -> acc @ [p]
in List.fold_left concat_one cura newa
......
[kernel] Parsing tests/rte/assign5.c (with preprocessing)
[kernel] Warning: Drop '*p' \from at tests/rte/assign5.c:9 for more precise one at tests/rte/assign5.c:10
[kernel] Warning: Drop '*p' \from at tests/rte/assign5.c:19 for more precise one at tests/rte/assign5.c:18
[rte] annotating function main
/* Generated by Frama-C */
/*@ assigns *p;
......
[kernel] Parsing tests/syntax/multiple_froms.i (no preprocessing)
[kernel] Warning: Drop 'b' \from at tests/syntax/multiple_froms.i:9 for more precise one at tests/syntax/multiple_froms.i:10
[kernel] Warning: Drop 'a' \from at tests/syntax/multiple_froms.i:7 for more precise one at tests/syntax/multiple_froms.i:6
/* Generated by Frama-C */
int a;
int b;
......
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