diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 3de84577103cb1b6bd7e3a17211be13da4001d09..826000ae54ffa9595eedb80f6b79a4ffc35b6861 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 aa1ba789ca9fca267ec802decd82a0ed1c226e9d..4eb800ca12dab45e1da5907e8bb2d64eaaca7983 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 05c8abe3fa6d930520097aa9c3b94a8f07000f3e..f66dc175d39c9a6d08950bd025d00bf455a6c564 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 a27bf94011e4a4341faf3a7e948d360ce70ec2d4..7fbc16abc9fc42a0b75856d8b054f318582f9da1 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));
+}