diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 9935cb8c1f1787727d2ca7fa15199e68f29df348..4bd3d232a6e0eecef3971e71c3970df8eff36300 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -7903,6 +7903,7 @@ and doInitializer loc local_env (vi: varinfo) (inite: Cabs.init_expression)
* the initializer (for local intialization)
*)
: chunk * init * typ * Cil_datatype.Lval.Set.t =
+ let open Current_loc.Operators in
let checkArrayInit ty init =
if Cil.isArrayType ty then
@@ -7923,7 +7924,8 @@ and doInitializer loc local_env (vi: varinfo) (inite: Cabs.init_expression)
let acc, preinit, restl =
let so = makeSubobj vi vi.vtype NoOffset in
let asconst = if vi.vglob then CConst else CNoConst in
- doInit loc local_env asconst NoInitPre so
+ let<> UpdatedCurrentLoc = loc in
+ doInit local_env asconst NoInitPre so
(unspecified_chunk empty) [ (Cabs.NEXT_INIT, inite) ]
in
if restl <> [] then
@@ -7959,10 +7961,7 @@ and doInitializer loc local_env (vi: varinfo) (inite: Cabs.init_expression)
– preinit corresponding to the complete initialization
– the list of unused initializers if any (should be empty most of the time)
*)
-and doInit loc local_env asconst preinit so acc initl =
- let open Current_loc.Operators in
- let<> UpdatedCurrentLoc = loc in
- let source = fst loc in
+and doInit local_env asconst preinit so acc initl =
let ghost = local_env.is_ghost in
let whoami fmt = Cil_printer.pp_lval fmt (Var so.host, so.soOff) in
let initl1 =
@@ -8068,14 +8067,14 @@ and doInit loc local_env asconst preinit so acc initl =
so'.stack <- [InArray(so'.curOff, bt, leno, ref 0)];
normalSubobj so';
let acc', preinit', initl' =
- doInit loc local_env asconst preinit so' acc charinits in
+ doInit local_env asconst preinit so' acc charinits in
if initl' <> [] then
- Kernel.warning ~source
+ Kernel.warning ~source:(fst e.expr_loc)
"Too many initializers for character array %t" whoami;
(* Advance past the array *)
advanceSubobj so;
(* Continue *)
- doInit loc local_env asconst preinit' so acc' restil
+ doInit local_env asconst preinit' so acc' restil
(* If we are at an array of WIDE characters and the initializer is a
* WIDE string literal (optionally enclosed in braces) then explore
* the WIDE string into characters *)
@@ -8141,7 +8140,7 @@ and doInit loc local_env asconst preinit so acc initl =
so'.stack <- [InArray(so'.curOff, bt, leno, ref 0)];
normalSubobj so';
let acc', preinit', initl' =
- doInit loc local_env asconst preinit so' acc charinits
+ doInit local_env asconst preinit so' acc charinits
in
if initl' <> [] then
(* sm: see above regarding ISO 6.7.8 para 14, which is not implemented
@@ -8152,7 +8151,7 @@ and doInit loc local_env asconst preinit so acc initl =
(* Advance past the array *)
advanceSubobj so;
(* Continue *)
- doInit loc local_env asconst preinit' so acc' restil
+ doInit local_env asconst preinit' so acc' restil
(* If we are at an array and we see a single initializer then it must
* be one for the first element *)
| TArray(bt, leno, _), (Cabs.NEXT_INIT, Cabs.SINGLE_INIT _oneinit) :: _restil ->
@@ -8161,12 +8160,12 @@ and doInit loc local_env asconst preinit so acc initl =
so.stack <- InArray(so.soOff, bt, leno, ref 0) :: so.stack;
normalSubobj so;
(* Start over with the fields *)
- doInit loc local_env asconst preinit so acc allinitl
+ doInit local_env asconst preinit so acc allinitl
(* An incomplete structure with any initializer is an error. *)
| TComp (comp, _), _ :: restil when comp.cfields = None ->
Kernel.error ~current:true ~once:true
"variable `%s' has initializer but incomplete type" so.host.vname;
- doInit loc local_env asconst preinit so acc restil
+ doInit local_env asconst preinit so acc restil
(* If we are at a composite and we see a single initializer of the same
* type as the composite then grab it all. If the type is not the same
* then we must go on and try to initialize the fields *)
@@ -8184,12 +8183,12 @@ and doInit loc local_env asconst preinit so acc initl =
(* Advance to the next subobject *)
advanceSubobj so;
let se = acc @@@ (se, ghost) in
- doInit loc local_env asconst preinit so se restil
+ doInit local_env asconst preinit so se restil
end else begin (* Try to initialize fields *)
let toinit = fieldsToInit comp None in
so.stack <- InComp(so.soOff, comp, toinit) :: so.stack;
normalSubobj so;
- doInit loc local_env asconst preinit so acc allinitl
+ doInit local_env asconst preinit so acc allinitl
end
(* A scalar with a single initializer *)
@@ -8209,7 +8208,7 @@ and doInit loc local_env asconst preinit so acc initl =
(* Move on *)
advanceSubobj so;
let se = acc @@@ (se,ghost) in
- doInit loc local_env asconst preinit' so se restil
+ doInit local_env asconst preinit' so se restil
(* An array with a compound initializer. The initializer is for the
* array elements *)
| TArray (bt, leno, _), (Cabs.NEXT_INIT, Cabs.COMPOUND_INIT initl) :: restil ->
@@ -8231,8 +8230,7 @@ and doInit loc local_env asconst preinit so acc initl =
no need to change the chunk.*)
acc, preinit', []
| _ ->
- doInit
- loc local_env asconst preinit so' acc initl
+ doInit local_env asconst preinit so' acc initl
in
if initl' <> [] then
Kernel.warning ~current:true
@@ -8240,7 +8238,7 @@ and doInit loc local_env asconst preinit so acc initl =
(* Advance past the array *)
advanceSubobj so;
(* Continue *)
- doInit loc local_env asconst preinit' so acc' restil
+ doInit local_env asconst preinit' so acc' restil
(* We have a designator that tells us to select the matching union field.
* This is to support a GCC extension *)
| TComp(ci, _) as targ,
@@ -8264,15 +8262,13 @@ and doInit loc local_env asconst preinit so acc initl =
in
(* If this is a cast from union X to union X *)
if Typ.equal t'noattr (Cil.typeDeepDropAllAttributes targ) then
- doInit
- loc local_env asconst preinit so acc
+ doInit local_env asconst preinit so acc
[(Cabs.NEXT_INIT, Cabs.SINGLE_INIT oneinit)]
else
(* If this is a GNU extension with field-to-union cast find the field *)
let fi = findField (Option.value ~default:[] ci.cfields) in
(* Change the designator and redo *)
- doInit
- loc local_env asconst preinit so acc
+ doInit local_env asconst preinit so acc
[Cabs.INFIELD_INIT (fi.fname, Cabs.NEXT_INIT), Cabs.SINGLE_INIT oneinit]
(* A structure with a composite initializer. We initialize the fields*)
@@ -8290,14 +8286,14 @@ and doInit loc local_env asconst preinit so acc initl =
let preinit' = setOneInit preinit so'.curOff (empty_preinit()) in
acc, preinit', []
| _ ->
- doInit loc local_env asconst preinit so' acc initl
+ doInit local_env asconst preinit so' acc initl
in
if initl' <> [] then
Kernel.warning ~current:true "Too many initializers for structure";
(* Advance past the structure *)
advanceSubobj so;
(* Continue *)
- doInit loc local_env asconst preinit' so acc' restil
+ doInit local_env asconst preinit' so acc' restil
(* A scalar with a initializer surrounded by a number of braces *)
| t, (Cabs.NEXT_INIT, next) :: restil ->
begin
@@ -8319,7 +8315,7 @@ and doInit loc local_env asconst preinit so acc initl =
(* Move on *)
advanceSubobj so;
let se = acc @@@ (se, ghost) in
- doInit loc local_env asconst preinit' so se restil
+ doInit local_env asconst preinit' so se restil
with Not_found ->
abort_context
"scalar value (of type %a) initialized by compound initializer"
@@ -8350,6 +8346,7 @@ and doInit loc local_env asconst preinit so acc initl =
end
| Cabs.ATINDEX_INIT(idx, whatnext) -> begin
+ let open Current_loc.Operators in
let<> UpdatedCurrentLoc = idx.expr_loc in
match unrollType so.soTyp with
| TArray (bt, leno, _) ->
@@ -8397,6 +8394,7 @@ and doInit loc local_env asconst preinit so acc initl =
| Cabs.ATINDEX_INIT (idx, whatnext) ->
expandRange (fun what -> top (Cabs.ATINDEX_INIT(idx, what))) whatnext
| Cabs.ATINDEXRANGE_INIT (idxs, idxe) ->
+ let open Current_loc.Operators in
let (rs, doidxs, idxs', _) =
doExp (no_paren_local_env local_env) CConst idxs (AExp(Some intType))
in
@@ -8430,12 +8428,10 @@ and doInit loc local_env asconst preinit so acc initl =
Cabs.NEXT_INIT)), ie)
:: loop (i + 1)
in
- doInit
- loc local_env asconst preinit so acc (loop first)
+ doInit local_env asconst preinit so acc (loop first)
| Cabs.NEXT_INIT -> (* We have not found any RANGE *)
let acc' = addressSubobj so what acc in
- doInit
- loc local_env asconst preinit so acc'
+ doInit local_env asconst preinit so acc'
((Cabs.NEXT_INIT, ie) :: restil)
in
expandRange (fun x -> x) what