diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 91c4994af7090ed7eaac006847dc3abe015ec2f3..4d0547747572c9c15ca8cd41bc96258efa779869 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 0000000000000000000000000000000000000000..1509fed0168da611a166d2f3320fcd89adca5c6d --- /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 0000000000000000000000000000000000000000..e788849228a210e64399d4c01a7acb1dcf39801b --- /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 +}