From e5c1c5ac922bf2427da8dcc6b8d234dd98da0907 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 2 Apr 2024 17:20:00 +0200
Subject: [PATCH] Remove unused add_implicit_ensures parameter from doInit
---
src/kernel_internals/typing/cabs2cil.ml | 43 ++++++++++++-------------
1 file changed, 20 insertions(+), 23 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 0a6d498f7f9..9935cb8c1f1 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -7923,7 +7923,7 @@ 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 Extlib.nop NoInitPre so
+ doInit loc local_env asconst NoInitPre so
(unspecified_chunk empty) [ (Cabs.NEXT_INIT, inite) ]
in
if restl <> [] then
@@ -7948,9 +7948,6 @@ and doInitializer loc local_env (vi: varinfo) (inite: Cabs.init_expression)
– local_env is the current environment
– asconst is used to indicate that expressions must be compile-time constant
(i.e. we are in a global initializer)
- – add_implicit_ensures is a callback to add an ensures clause to contracts
- above current initialized part when it is partially initialized.
- Does nothing initially. Useful only for initialization of locals
– preinit corresponds to the initializers seen previously (for globals)
– so contains the information about the current subobject currently being
initialized
@@ -7962,7 +7959,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 add_implicit_ensures preinit so acc initl =
+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
@@ -8071,14 +8068,14 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
so'.stack <- [InArray(so'.curOff, bt, leno, ref 0)];
normalSubobj so';
let acc', preinit', initl' =
- doInit loc local_env asconst add_implicit_ensures preinit so' acc charinits in
+ doInit loc local_env asconst preinit so' acc charinits in
if initl' <> [] then
Kernel.warning ~source
"Too many initializers for character array %t" whoami;
(* Advance past the array *)
advanceSubobj so;
(* Continue *)
- doInit loc local_env asconst add_implicit_ensures preinit' so acc' restil
+ doInit loc 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 *)
@@ -8144,7 +8141,7 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
so'.stack <- [InArray(so'.curOff, bt, leno, ref 0)];
normalSubobj so';
let acc', preinit', initl' =
- doInit loc local_env asconst add_implicit_ensures preinit so' acc charinits
+ doInit loc 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
@@ -8155,7 +8152,7 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
(* Advance past the array *)
advanceSubobj so;
(* Continue *)
- doInit loc local_env asconst add_implicit_ensures preinit' so acc' restil
+ doInit loc 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 ->
@@ -8164,12 +8161,12 @@ and doInit loc local_env asconst add_implicit_ensures 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 add_implicit_ensures preinit so acc allinitl
+ doInit loc 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 add_implicit_ensures preinit so acc restil
+ doInit loc 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 *)
@@ -8187,12 +8184,12 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
(* Advance to the next subobject *)
advanceSubobj so;
let se = acc @@@ (se, ghost) in
- doInit loc local_env asconst add_implicit_ensures preinit so se restil
+ doInit loc 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 add_implicit_ensures preinit so acc allinitl
+ doInit loc local_env asconst preinit so acc allinitl
end
(* A scalar with a single initializer *)
@@ -8212,7 +8209,7 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
(* Move on *)
advanceSubobj so;
let se = acc @@@ (se,ghost) in
- doInit loc local_env asconst add_implicit_ensures preinit' so se restil
+ doInit loc 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 ->
@@ -8235,7 +8232,7 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
acc, preinit', []
| _ ->
doInit
- loc local_env asconst add_implicit_ensures preinit so' acc initl
+ loc local_env asconst preinit so' acc initl
in
if initl' <> [] then
Kernel.warning ~current:true
@@ -8243,7 +8240,7 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
(* Advance past the array *)
advanceSubobj so;
(* Continue *)
- doInit loc local_env asconst add_implicit_ensures preinit' so acc' restil
+ doInit loc 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,
@@ -8268,14 +8265,14 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
(* 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 add_implicit_ensures preinit so acc
+ loc 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 add_implicit_ensures preinit so acc
+ loc 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*)
@@ -8293,14 +8290,14 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
let preinit' = setOneInit preinit so'.curOff (empty_preinit()) in
acc, preinit', []
| _ ->
- doInit loc local_env asconst add_implicit_ensures preinit so' acc initl
+ doInit loc 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 add_implicit_ensures preinit' so acc' restil
+ doInit loc 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
@@ -8322,7 +8319,7 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
(* Move on *)
advanceSubobj so;
let se = acc @@@ (se, ghost) in
- doInit loc local_env asconst add_implicit_ensures preinit' so se restil
+ doInit loc local_env asconst preinit' so se restil
with Not_found ->
abort_context
"scalar value (of type %a) initialized by compound initializer"
@@ -8434,11 +8431,11 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
:: loop (i + 1)
in
doInit
- loc local_env asconst add_implicit_ensures preinit so acc (loop first)
+ loc 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 add_implicit_ensures preinit so acc'
+ loc local_env asconst preinit so acc'
((Cabs.NEXT_INIT, ie) :: restil)
in
expandRange (fun x -> x) what
--
GitLab