diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 3925038637dae16b4853526a89536646f171eee8..16f71399f19c2c62203af174b1534000e037294e 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -3364,6 +3364,7 @@ let integerArrayLength (leno: exp option) : int = try lenOfArray leno with | LenOfArray cause -> + Cil.CurrentLoc.set len.eloc; abort_context "Array length %a is %a: no explicit initializer allowed." Cil_printer.pp_exp len Cil.pp_incorrect_array_length cause diff --git a/tests/syntax/oracle/very_large_integers.14.res.oracle b/tests/syntax/oracle/very_large_integers.14.res.oracle index 7cbdaf67c3bf4023f8a9718c4fdf3ad4a994aee4..5846557a229caea20c1f6c9a067d5dcd383a5a5d 100644 --- a/tests/syntax/oracle/very_large_integers.14.res.oracle +++ b/tests/syntax/oracle/very_large_integers.14.res.oracle @@ -4,7 +4,7 @@ [kernel] very_large_integers.c:84: Warning: ignoring invalid aligned attribute: __aligned__((9223372036854775808)+ (9223372036854775808) ) -[kernel] very_large_integers.c:106: User Error: Array length is too large. +[kernel] very_large_integers.c:107: User Error: Array length is too large. [kernel] very_large_integers.c:114: User Error: array length too large: 7205759403792794 112 // Previously caused Out of memory diff --git a/tests/syntax/oracle/very_large_integers.4.res.oracle b/tests/syntax/oracle/very_large_integers.4.res.oracle index 77a8b542245f0fbe7d3a2607a9f110cf9a092df9..f30af367582a82c726be86d33ea3487afffee4a2 100644 --- a/tests/syntax/oracle/very_large_integers.4.res.oracle +++ b/tests/syntax/oracle/very_large_integers.4.res.oracle @@ -5,7 +5,7 @@ 60 61 #ifdef INIT_DESIGNATOR 62 int arr2[9999999999999999999U] = { [9999999999999999999U] = 42 }; - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^^^^^^ 63 #endif 64 [kernel] Frama-C aborted: invalid user input.