From 175a57bbe8ccafcc8f0f975c31b8a7154a267548 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 21 Jun 2022 15:30:17 +0200
Subject: [PATCH] [kernel] Normalize also ill-formed types entries in TypSize
cache
Not sure if the loop could occur here as well, but it can't hurt anyway
---
src/kernel_services/ast_queries/cil.ml | 17 ++++++++++-------
1 file changed, 10 insertions(+), 7 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index a3fd3727f08..9f02a5b5590 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3960,8 +3960,8 @@ let find_sizeof t f =
let t', size = f () in
TypSize.add t' (Size size) ;
size
- with SizeOfError(t',msg) as e ->
- TypSize.add t (Error (t', msg)) ;
+ with SizeOfError(msg, t') as e ->
+ TypSize.add t' (Error (msg, t')) ;
raise e
let selfTypSize = TypSize.self
@@ -4434,8 +4434,10 @@ and bitsSizeOf t =
find_sizeof t
(fun () ->
begin
- match constFold true len with
- { enode = Const(CInt64(l,_,_)) } as v->
+ let v = constFold true len in
+ let norm_typ = TArray(bt, Some v, attrs) in
+ match v with
+ { enode = Const(CInt64(l,_,_)) } ->
let sz = Integer.mul (Integer.of_int (bitsSizeOf bt)) l in
let sz' =
match Integer.to_int_opt sz with
@@ -4444,11 +4446,12 @@ and bitsSizeOf t =
raise
(SizeOfError
("Array is so long that its size can't be "
- ^"represented with an OCaml int.", t))
+ ^"represented with an OCaml int.", norm_typ))
in
- (TArray(bt, Some v,attrs), sz') (*WAS: addTrailing sz' (8 * bytesAlignOf t)*)
- | _ -> raise (SizeOfError ("Array with non-constant length.", t))
+ (norm_typ, sz') (*WAS: addTrailing sz' (8 * bytesAlignOf t)*)
+ | _ ->
+ raise (SizeOfError ("Array with non-constant length.", norm_typ))
end)
| TVoid _ ->
if theMachine.theMachine.sizeof_void >= 0 then
--
GitLab