From b566a307f3ad19a0653d04368bb28f08a5944ff3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 21 Apr 2021 11:08:16 +0200
Subject: [PATCH] [kernel] Fails on sizeof(void) when the machdep does not
define sizeof_void.
Fails uniformly on sizeof(void) and sizeof applied to expressions of type void.
---
src/kernel_internals/typing/cabs2cil.ml | 37 ++++++++-----------
.../oracle/function_ptr_alignof.res.oracle | 2 +-
2 files changed, 16 insertions(+), 23 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4a6cd9920cc..4ea05a8eabf 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1336,6 +1336,15 @@ let canDropStatement (s: stmt) : bool =
ignore (visitCilStmt vis s);
!pRes
+let fail_if_incompatible_sizeof ~ensure_complete op typ =
+ if Cil.isFunctionType typ && Cil.theMachine.theMachine.sizeof_fun < 0 then
+ Kernel.error ~current:true "%s called on function" op;
+ let is_void = Cil.isVoidType typ in
+ if is_void && Cil.theMachine.theMachine.sizeof_void < 0 then
+ Kernel.error ~current:true "%s on void type" op;
+ if ensure_complete && not (Cil.isCompleteType typ) && not is_void then
+ Kernel.error ~current:true
+ "%s on incomplete type '%a'" op Cil_printer.pp_typ typ
(******** CASTS *********)
@@ -6007,14 +6016,8 @@ and doExp local_env
| A.TYPE_SIZEOF (bt, dt) ->
let typ = doOnlyType local_env.is_ghost bt dt in
- let res =
- if Cil.isCompleteType typ then new_exp ~loc (SizeOf typ)
- else begin
- Kernel.error ~once:true ~current:true
- "sizeof on incomplete type '%a'" Cil_printer.pp_typ typ;
- new_exp ~loc (Const (CStr ("booo sizeof(incomplete)")))
- end
- in
+ fail_if_incompatible_sizeof ~ensure_complete:true "sizeof" typ;
+ let res = new_exp ~loc (SizeOf typ) in
finishExp [] (unspecified_chunk empty) res theMachine.typeOfSizeOf
| A.EXPR_SIZEOF e ->
@@ -6023,9 +6026,7 @@ and doExp local_env
let (_, se, e', lvt) =
doExp (no_paren_local_env local_env) CNoConst e AExpLeaveArrayFun
in
- if Cil.isFunctionType lvt && Cil.theMachine.theMachine.sizeof_fun < 0 then
- Kernel.abort ~current:true
- "sizeof() called on function";
+ fail_if_incompatible_sizeof ~ensure_complete:false "sizeof()" lvt;
let scope_chunk = drop_chunk "sizeof" se e e' in
let size =
match e'.enode with
@@ -6042,23 +6043,15 @@ and doExp local_env
| A.TYPE_ALIGNOF (bt, dt) ->
let typ = doOnlyType local_env.is_ghost bt dt in
- let res =
- if Cil.isCompleteType typ then new_exp ~loc (AlignOf typ)
- else begin
- Kernel.error ~once:true ~current:true
- "sizeof on incomplete type '%a'" Cil_printer.pp_typ typ;
- new_exp ~loc (Const (CStr ("booo alignof(incomplete)")))
- end
- in
+ fail_if_incompatible_sizeof ~ensure_complete:true "alignof" typ;
+ let res = new_exp ~loc (AlignOf typ) in
finishExp [] (unspecified_chunk empty) res theMachine.typeOfSizeOf
| A.EXPR_ALIGNOF e ->
let (_, se, e', lvt) =
doExp (no_paren_local_env local_env) CNoConst e AExpLeaveArrayFun
in
- if Cil.isFunctionType lvt && Cil.theMachine.theMachine.alignof_fun < 0
- then
- Kernel.abort ~current:true "alignof() called on a function.";
+ fail_if_incompatible_sizeof ~ensure_complete:false "alignof()" lvt;
let scope_chunk = drop_chunk "alignof" se e e' in
let e'' =
match e'.enode with (* If we are taking the alignof an
diff --git a/tests/misc/oracle/function_ptr_alignof.res.oracle b/tests/misc/oracle/function_ptr_alignof.res.oracle
index b7d7520c167..3bdec0691bd 100644
--- a/tests/misc/oracle/function_ptr_alignof.res.oracle
+++ b/tests/misc/oracle/function_ptr_alignof.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/misc/function_ptr_alignof.i (no preprocessing)
[kernel] tests/misc/function_ptr_alignof.i:13: User Error:
- alignof() called on a function.
+ alignof() called on function
[kernel] User Error: stopping on file "tests/misc/function_ptr_alignof.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
--
GitLab