diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 7f288f6aea6f9348aa7de2247856d190f2fe5d65..833e0631f2cf8ac3946248d27c4fbfa30dd3aef8 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -498,21 +498,24 @@ global:
/* (* Old-style function prototype. This should be somewhere else, like in
* "declaration". For now we keep it at global scope only because in local
* scope it looks too much like a function call *) */
-| IDENT LPAREN old_parameter_list_ne RPAREN old_pardef_list SEMICOLON
- {
- let loc = Cil_datatype.Location.of_lexing_loc $loc($1) in
- (* Convert pardecl to new style *)
- let pardecl, isva = doOldParDecl $3 $5 in
- (* Make the function declarator *)
- doDeclaration None loc []
- [(($1, PROTO(JUSTBASE, pardecl,[],isva),
- ["FC_OLDSTYLEPROTO",[]], loc), NO_INIT)]
- }
-| IDENT LPAREN RPAREN SEMICOLON {
- let loc = Cil_datatype.Location.of_lexing_loc $loc($1) in
- doDeclaration None loc []
- [(($1, PROTO(JUSTBASE,[],[],false),
- ["FC_OLDSTYLEPROTO",[]], loc), NO_INIT)]
+| f=IDENT LPAREN prms=old_parameter_list_ne RPAREN
+ decls=old_pardef_list SEMICOLON
+ {
+ let dloc = Cil_datatype.Location.of_lexing_loc $loc in
+ let floc = Cil_datatype.Location.of_lexing_loc $loc(f) in
+ (* Convert pardecl to new style *)
+ let pardecl, isva = doOldParDecl prms decls in
+ (* Make the function declarator *)
+ doDeclaration None dloc []
+ [((f, PROTO(JUSTBASE, pardecl,[],isva),
+ ["FC_OLDSTYLEPROTO",[]], floc), NO_INIT)]
+ }
+| f=IDENT LPAREN RPAREN SEMICOLON {
+ let dloc = Cil_datatype.Location.of_lexing_loc $loc in
+ let floc = Cil_datatype.Location.of_lexing_loc $loc(f) in
+ doDeclaration None dloc []
+ [((f, PROTO(JUSTBASE,[],[],false),
+ ["FC_OLDSTYLEPROTO",[]], floc), NO_INIT)]
}
;
@@ -1068,31 +1071,39 @@ ghost_parameter:
;
declaration: /* ISO 6.7.*/
- decl_spec_list init_declarator_list SEMICOLON
- { doDeclaration None ((snd $1)) (fst $1) $2 }
-| decl_spec_list SEMICOLON
- { if !Lexerhack.is_typedef () then begin
- let source =
- Cil_datatype.Position.of_lexing_pos $startpos($1)
- in
- Kernel.warning ~source ~wkey:Kernel.wkey_unnamed_typedef
- "typedef without a name"
+ specif=decl_spec_list decls=init_declarator_list SEMICOLON
+ {
+ let loc = Cil_datatype.Location.of_lexing_loc $loc in
+ doDeclaration None loc (fst specif) decls
+ }
+| decls=decl_spec_list SEMICOLON
+ {
+ let loc = Cil_datatype.Location.of_lexing_loc $loc in
+ if !Lexerhack.is_typedef () then begin
+ let source = fst loc in
+ let wkey = Kernel.wkey_unnamed_typedef in
+ Kernel.warning ~source ~wkey "typedef without a name"
end;
!Lexerhack.reset_typedef();
- doDeclaration None ((snd $1)) (fst $1) []
+ doDeclaration None loc (fst decls) []
}
-| SPEC decl_spec_list init_declarator_list SEMICOLON
- { doDeclaration (Some $1) ((snd $2)) (fst $2) $3 }
-| SPEC decl_spec_list SEMICOLON
- { if !Lexerhack.is_typedef () then begin
+| spec=SPEC specif=decl_spec_list decls=init_declarator_list SEMICOLON
+ {
+ let loc = Cil_datatype.Location.of_lexing_loc $loc in
+ doDeclaration (Some spec) loc (fst specif) decls
+ }
+| spec=SPEC specif=decl_spec_list SEMICOLON
+ {
+ let loc = Cil_datatype.Location.of_lexing_loc $loc in
+ if !Lexerhack.is_typedef () then begin
let source =
- Cil_datatype.Position.of_lexing_pos $startpos($2)
+ Cil_datatype.Position.of_lexing_pos $startpos(specif)
in
- Kernel.warning ~source ~wkey:Kernel.wkey_unnamed_typedef
- "typedef without a name"
+ let wkey = Kernel.wkey_unnamed_typedef in
+ Kernel.warning ~source ~wkey "typedef without a name"
end;
!Lexerhack.reset_typedef();
- doDeclaration (Some $1) ((snd $2)) (fst $2) [] }
+ doDeclaration (Some spec) loc (fst specif) [] }
| static_assert_declaration SEMICOLON
{ let (e, m, loc) = $1 in STATIC_ASSERT (e, m, loc) }
;
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index e853f79ce7bc022e64cc60f8678a90a8e0f1d54d..f99ddf62868dd2dadc831c14c2fdf5204d196304 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -7910,8 +7910,6 @@ and doInitializer loc local_env (vi: varinfo) (inite: Cabs.init_expression)
*)
: chunk * init * typ * Cil_datatype.Lval.Set.t =
- CurrentLoc.set loc;
-
let checkArrayInit ty init =
if Cil.isArrayType ty then
match init with
@@ -7971,6 +7969,7 @@ and doInitializer loc local_env (vi: varinfo) (inite: Cabs.init_expression)
– the list of unused initializers if any (should be empty most of the time)
*)
and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
+ CurrentLoc.set loc;
let source = fst loc in
let ghost = local_env.is_ghost in
let whoami fmt = Cil_printer.pp_lval fmt (Var so.host, so.soOff) in
@@ -9050,6 +9049,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
(* Do all the variables and concatenate the resulting statements *)
let doOneDeclarator (acc: chunk) (name: init_name) =
let (n,ndt,a,l),_ = name in
+ CurrentLoc.set l;
if isglobal then begin
let bt,_,_,attrs = spec_res in
let vtype, nattr =
@@ -9057,14 +9057,14 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
(AttrName false) bt (Cabs.PARENTYPE(attrs, ndt, a)) in
(match filterAttributes "alias" nattr with
| [] -> (* ordinary prototype. *)
- ignore (createGlobal cloc local_env.is_ghost logic_spec spec_res name)
+ ignore (createGlobal l local_env.is_ghost logic_spec spec_res name)
(* E.log "%s is not aliased\n" name *)
| [Attr("alias", [AStr othername])] ->
if not (isFunctionType vtype) || local_env.is_ghost then begin
Kernel.warning ~current:true
"%a: CIL only supports attribute((alias)) for C functions."
Cil_printer.pp_location (CurrentLoc.get ());
- ignore (createGlobal cloc ghost logic_spec spec_res name)
+ ignore (createGlobal l ghost logic_spec spec_res name)
end else
doAliasFun ghost vtype n othername (s, (n,ndt,a,l)) loc
| _ ->
diff --git a/tests/misc/oracle/pragma-pack.0.res.oracle b/tests/misc/oracle/pragma-pack.0.res.oracle
index 496ab33d0b3a9a832384820acac75e32ffa57341..ad555d0abd1141433579884bf370aa2f0b3c7627 100644
--- a/tests/misc/oracle/pragma-pack.0.res.oracle
+++ b/tests/misc/oracle/pragma-pack.0.res.oracle
@@ -91,7 +91,7 @@
adding aligned(4) attribute to field '__anonstruct_test1_1.k' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:140:
adding aligned(1) attribute to field '__anonstruct_test1_1.l' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:136:
+[kernel:typing:pragma] pragma-pack.c:141:
adding aligned(4) attribute to comp '__anonstruct_test1_1' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:142: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:152:
@@ -104,7 +104,7 @@
adding aligned(1) attribute to field '__anonstruct_test2_3.k' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:157:
adding aligned(1) attribute to field '__anonstruct_test2_3.l' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:153:
+[kernel:typing:pragma] pragma-pack.c:158:
adding aligned(1) attribute to comp '__anonstruct_test2_3' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:159: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:169:
@@ -139,7 +139,7 @@
adding aligned(2) attribute to field '__anonstruct_test7_13.k' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:244:
adding aligned(1) attribute to field '__anonstruct_test7_13.l' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:238:
+[kernel:typing:pragma] pragma-pack.c:245:
adding aligned(2) attribute to comp '__anonstruct_test7_13' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:247:
adding aligned(2) attribute to field '__anonstruct_test7_2_14.i' due to packing pragma
@@ -149,7 +149,7 @@
adding aligned(2) attribute to field '__anonstruct_test7_2_14.k' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:250:
adding aligned(2) attribute to field '__anonstruct_test7_2_14.l' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:246:
+[kernel:typing:pragma] pragma-pack.c:251:
adding aligned(2) attribute to comp '__anonstruct_test7_2_14' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:252: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:336:
@@ -158,7 +158,7 @@
adding aligned(1) attribute to field '__anonstruct_barcode_bmp_t_18.len' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:339:
adding aligned(1) attribute to field '__anonstruct_barcode_bmp_t_18.data' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:337:
+[kernel:typing:pragma] pragma-pack.c:340:
adding aligned(1) attribute to comp '__anonstruct_barcode_bmp_t_18' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:341: packing pragma: popped alignment 16
[eva] Analyzing a complete application starting at main
diff --git a/tests/syntax/oracle/fam.res.oracle b/tests/syntax/oracle/fam.res.oracle
index 9ce16b157f1404aa2a26cd754b7fdf028572c2d1..55eb9b89b58a3ee32fa7fa58cd00993ad81f2c7b 100644
--- a/tests/syntax/oracle/fam.res.oracle
+++ b/tests/syntax/oracle/fam.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing fam.i (no preprocessing)
-[kernel] fam.i:16: User Error:
+[kernel] fam.i:19: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] fam.i:29: User Error:
field `b' is declared with incomplete type char []
-[kernel] fam.i:28: User Error:
+[kernel] fam.i:31: User Error:
static initialization of flexible array members is an unsupported GNU extension
-[kernel] fam.i:49: User Error:
+[kernel] fam.i:56: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] fam.i:63: User Error:
static initialization of flexible array members is an unsupported GNU extension
diff --git a/tests/syntax/oracle/func_locs.res.oracle b/tests/syntax/oracle/func_locs.res.oracle
index 8fd4ca099e2fa45737df2beec4c827b0473d0f65..3a3c61326536ab13d1b041577c80b9912a250734 100644
--- a/tests/syntax/oracle/func_locs.res.oracle
+++ b/tests/syntax/oracle/func_locs.res.oracle
@@ -3,8 +3,8 @@
found two contracts (old location: func_locs.i:13). Merging them
func_locs.i:31 char 3 - func_locs.i:36 char 1 -> main
func_locs.i:27 char 4 - func_locs.i:29 char 1 -> def_no_spec
-func_locs.i:25 char 20 - func_locs.i:25 char 26 -> id
-func_locs.i:25 char 0 - func_locs.i:25 char 16 -> decl_no_spec
+func_locs.i:25 char 24 - func_locs.i:25 char 26 -> id
+func_locs.i:25 char 4 - func_locs.i:25 char 16 -> decl_no_spec
func_locs.i:20 char 3 - func_locs.i:23 char 6 -> id
func_locs.i:13 char 3 - func_locs.i:18 char 6 -> id
func_locs.i:7 char 3 - func_locs.i:9 char 1 -> with_spec
diff --git a/tests/syntax/oracle/static_assert_wrong.res.oracle b/tests/syntax/oracle/static_assert_wrong.res.oracle
index d2e83bab9e6ee0bdc2ab1f40b164d1f5e2617354..6b70ee159b2a50426081d077d4c4b491b89c3d45 100644
--- a/tests/syntax/oracle/static_assert_wrong.res.oracle
+++ b/tests/syntax/oracle/static_assert_wrong.res.oracle
@@ -1,9 +1,11 @@
[kernel] Parsing static_assert_wrong.i (no preprocessing)
-[kernel] static_assert_wrong.i:8:
+[kernel] static_assert_wrong.i:6:
syntax error:
- Location: line 8, between columns 0 and 3, before or at token: int
+ Location: between lines 6 and 8, before or at token: int
+ 4 */
+ 5
+
6 _Static_assert(1,"assert succeeds")
7
8 int x = 0;
- ^^^
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/array_zero_length.2.res.oracle b/tests/value/oracle/array_zero_length.2.res.oracle
index 62bce111ca998c475103f11cedc7d16c75c6b07a..440a1beac59d2fbcb72a118f60ae03d9d4638e1f 100644
--- a/tests/value/oracle/array_zero_length.2.res.oracle
+++ b/tests/value/oracle/array_zero_length.2.res.oracle
@@ -11,7 +11,7 @@
11 char W[][0];
12
13 char T1[] = {};
- ^^^^^^^^^^^^^^^
+ ^^
14 char U1[0] = {};
15 char V1[][2] = {};
[kernel] Frama-C aborted: invalid user input.