From 721c3c66ba006da03d26cdab86b3dc6b9a9d1646 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 10 Sep 2024 13:58:16 +0200
Subject: [PATCH] [cabs2cil] avoid crash in syntactically invalid code, switch
with a double
---
src/kernel_internals/typing/cabs2cil.ml | 2 +-
tests/syntax/oracle/switch-float.res.oracle | 3 +++
tests/syntax/switch-float.i | 9 +++++++++
3 files changed, 13 insertions(+), 1 deletion(-)
create mode 100644 tests/syntax/oracle/switch-float.res.oracle
create mode 100644 tests/syntax/switch-float.i
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 91c4994af7..4d05477475 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -10047,7 +10047,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
let loc' = convLoc loc in
let (se, e', et) = doFullExp local_env CNoConst e (AExp None) in
if not (Cil.isIntegralType et) then
- Kernel.error ~once:true ~current:true "Switch on a non-integer expression.";
+ Kernel.abort ~once:true ~current:true "Switch on a non-integer expression.";
let et' = Cil.integralPromotion et in
let e' = mkCastT ~oldt:et ~newt:et' e' in
enter_break_env ();
diff --git a/tests/syntax/oracle/switch-float.res.oracle b/tests/syntax/oracle/switch-float.res.oracle
new file mode 100644
index 0000000000..1509fed016
--- /dev/null
+++ b/tests/syntax/oracle/switch-float.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing switch-float.i (no preprocessing)
+[kernel] switch-float.i:8: User Error: Switch on a non-integer expression.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/switch-float.i b/tests/syntax/switch-float.i
new file mode 100644
index 0000000000..e788849228
--- /dev/null
+++ b/tests/syntax/switch-float.i
@@ -0,0 +1,9 @@
+/* run.config
+ EXIT: 1
+ STDOPT:
+*/
+
+void switch_float() {
+ double x = -1.5;
+ switch (x); // invalid, but must not crash
+}
--
GitLab