diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly index 121ad96facc0f37bf6de65c4c7f03e57953649fb..9b7cde38cfcb240c6cadf5909daef03a5cfbfc32 100644 --- a/src/kernel_internals/parsing/logic_parser.mly +++ b/src/kernel_internals/parsing/logic_parser.mly @@ -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 diff --git a/tests/syntax/multiple_assigns.i b/tests/syntax/multiple_assigns.i new file mode 100644 index 0000000000000000000000000000000000000000..d20a1dfcda46f0720ce70523677b4472dd709f80 --- /dev/null +++ b/tests/syntax/multiple_assigns.i @@ -0,0 +1,10 @@ +int z; + +/*@ assigns z, z; + assigns z \from z; + assigns z, z; + */ +void function(void) +{ + return; +} diff --git a/tests/syntax/oracle/multiple_assigns.res.oracle b/tests/syntax/oracle/multiple_assigns.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..0cda603d543618256b3d8bc527983157bf1538ed --- /dev/null +++ b/tests/syntax/oracle/multiple_assigns.res.oracle @@ -0,0 +1,11 @@ +[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; +} + +