diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 4e13f8455dde1898f6b597576558104751360eca..3925038637dae16b4853526a89536646f171eee8 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -8397,6 +8397,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl = in let doidxs = add_reads ~ghost idxs'.eloc rs doidxs in let doidxe = add_reads ~ghost idxe'.eloc re doidxe in + Cil.CurrentLoc.set (fst idxs'.eloc, snd idxe'.eloc); if isNotEmpty doidxs || isNotEmpty doidxe then abort_context "Range designators are not constants"; let first, last = diff --git a/tests/syntax/oracle/very_large_integers.6.res.oracle b/tests/syntax/oracle/very_large_integers.6.res.oracle index 8858cc405bb0645d7f38002cae3026c63d295700..a276df46d02a52e4e83faadd7a57ddb0b035a565 100644 --- a/tests/syntax/oracle/very_large_integers.6.res.oracle +++ b/tests/syntax/oracle/very_large_integers.6.res.oracle @@ -8,7 +8,7 @@ 68 69 #ifdef RANGE_DESIGNATOR 70 int arr4[1] = { [-9999999999999999999U ... 9999999999999999999U] = 42 }; - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 71 #endif 72 [kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/very_large_integers.7.res.oracle b/tests/syntax/oracle/very_large_integers.7.res.oracle index 22ddabcd753fb60429538a5af7d37fb3174b8581..9e0b1da102ea4f9ae9e17219f10d684ce6c480bf 100644 --- a/tests/syntax/oracle/very_large_integers.7.res.oracle +++ b/tests/syntax/oracle/very_large_integers.7.res.oracle @@ -4,7 +4,7 @@ 72 73 #ifdef RANGE_DESIGNATOR2 74 int widths[] = { [99999999999999999 ... 999999999999999999] = 2 }; - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 75 #endif 76 [kernel] Frama-C aborted: invalid user input.