From 81f0ff9784702c61c1d7df1a240eb3251fb92c5d Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 19 Jun 2024 15:35:26 +0200
Subject: [PATCH] [typing] ensure we can compute the sizeof of a VLA type

---
 src/kernel_internals/typing/cabs2cil.ml | 9 +++++----
 tests/syntax/oracle/sizeof.0.res.oracle | 9 +++++++++
 tests/syntax/oracle/sizeof.1.res.oracle | 9 +++++++++
 tests/syntax/sizeof.c                   | 8 ++++++++
 4 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 3de84577103..826000ae54f 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4451,8 +4451,7 @@ let rec doSpecList loc ghost (suggestedAnonName: string)
        *)
       t'
 
-    | [Cabs.TtypeofT (specs, dt)] ->
-      doOnlyType loc ghost specs dt
+    | [Cabs.TtypeofT (specs, dt)] -> doOnlyType loc ghost specs dt
 
     | l ->
       abort_context
@@ -5065,12 +5064,14 @@ and isVariableSizedArray ghost (dt: Cabs.decl_type)
   | None -> None
   | Some (se, e) -> Some (dt', se, e)
 
-and doOnlyType loc ghost (specs: Cabs.spec_elem list) (dt: Cabs.decl_type) : typ =
+and doOnlyType loc ghost specs dt =
   let bt',sto,inl,attrs = doSpecList loc ghost "" specs in
   if sto <> NoStorage || inl then
     Kernel.error ~once:true ~current:true "Storage or inline specifier in type only";
   let tres, nattr =
-    doType ghost `OnlyType AttrType bt' (Cabs.PARENTYPE(attrs, dt, [])) in
+    doType ghost `OnlyType AttrType bt' (Cabs.PARENTYPE(attrs, dt, []))
+      ~allowVarSizeArrays:true
+  in
   if nattr <> [] then
     Kernel.error ~once:true ~current:true
       "Name attributes in only_type: %a" Cil_printer.pp_attributes nattr;
diff --git a/tests/syntax/oracle/sizeof.0.res.oracle b/tests/syntax/oracle/sizeof.0.res.oracle
index aa1ba789ca9..4eb800ca12d 100644
--- a/tests/syntax/oracle/sizeof.0.res.oracle
+++ b/tests/syntax/oracle/sizeof.0.res.oracle
@@ -1,5 +1,6 @@
 [kernel] Parsing sizeof.c (with preprocessing)
 /* Generated by Frama-C */
+#include "assert.h"
 #include "stdint.h"
 char c = (char)1;
 char a = (char)'a';
@@ -14,4 +15,12 @@ uint64_t u64 = 6453UL;
 int v = 645201;
 float f = (float)1.;
 double d = 1.;
+void vla(int n)
+{
+  unsigned long s = sizeof(int [n]);
+  __FC_assert((s == (unsigned long)n * sizeof(int)) != 0,"sizeof.c",49,
+              "s == n * sizeof(int)");
+  return;
+}
+
 
diff --git a/tests/syntax/oracle/sizeof.1.res.oracle b/tests/syntax/oracle/sizeof.1.res.oracle
index 05c8abe3fa6..f66dc175d39 100644
--- a/tests/syntax/oracle/sizeof.1.res.oracle
+++ b/tests/syntax/oracle/sizeof.1.res.oracle
@@ -1,5 +1,6 @@
 [kernel] Parsing sizeof.c (with preprocessing)
 /* Generated by Frama-C */
+#include "assert.h"
 #include "stdint.h"
 char c = (char)1;
 char a = (char)'a';
@@ -14,4 +15,12 @@ uint64_t u64 = 6453ULL;
 int v = 645201;
 float f = (float)1.;
 double d = 1.;
+void vla(int n)
+{
+  unsigned long s = (unsigned long)sizeof(int [n]);
+  __FC_assert((s == (unsigned long)((unsigned int)n * sizeof(int))) != 0,
+              "sizeof.c",49,"s == n * sizeof(int)");
+  return;
+}
+
 
diff --git a/tests/syntax/sizeof.c b/tests/syntax/sizeof.c
index a27bf94011e..7fbc16abc9f 100644
--- a/tests/syntax/sizeof.c
+++ b/tests/syntax/sizeof.c
@@ -3,6 +3,9 @@
    STDOPT: -machdep x86_64
    STDOPT: -machdep x86_32
 */
+
+#include <assert.h>
+
 char c = 1;
 _Static_assert(sizeof(-c) == sizeof(int), "Integer promotion with minus");
 _Static_assert(sizeof(+c) == sizeof(int), "Integer promotion with plus");
@@ -40,3 +43,8 @@ float f = 1.;
 _Static_assert(sizeof +f == sizeof(float), "Float promotion");
 double d = 1.;
 _Static_assert(sizeof +d == sizeof(double), "Double promotion");
+
+void vla(int n) {
+  unsigned long s = sizeof(int[n]);
+  assert(s == n * sizeof(int));
+}
-- 
GitLab