Commit 3ce322ba authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[parser] Merge "assigns x, x, ..."

parent cf01dcb0
......@@ -151,7 +151,7 @@
| Writes [], _ | Writes _, [] ->
raise (
Not_well_formed (loc(),"Mixing \\nothing and a real location"))
| Writes a1, a2 -> Writes (concat_froms a2 a1)
| Writes a1, a2 -> Writes (concat_froms (concat_froms [] a2) a1)
let concat_loop_assigns_allocation annots bhvs2 a2 fa2=
(* NB: this is supposed to merge assigns related to named behaviors, in
......
int z;
/*@ assigns z, z;
assigns z \from z;
assigns z, z;
*/
void function(void)
{
return;
}
[kernel] Parsing tests/syntax/multiple_assigns.i (no preprocessing)
/* Generated by Frama-C */
int z;
/*@ assigns z;
assigns z \from z; */
void function(void)
{
return;
}
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