diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index c440701e41cd2e4d98ad1cab896990b17a35d205..d98f976c73898a1ec6b4cd9e749e7dc7405908c2 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -128,10 +128,11 @@ let typeForInsertedVar: (Cil_types.typ -> Cil_types.typ) ref = ref (fun t -> t)
let cabs_exp loc node = { expr_loc = loc; expr_node = node }
let abort_context msg =
- let pos = fst (Cil.CurrentLoc.get ()) in
+ let (p1,p2) = Cil.CurrentLoc.get() in
let append fmt =
Format.pp_print_newline fmt ();
- Errorloc.pp_context_from_file fmt pos
+ Errorloc.pp_context_from_file
+ ~start_line:p1.pos_lnum ~start_char:(p1.pos_cnum -p1.pos_bol) fmt p2
in
Kernel.abort ~current:true ~append msg
@@ -2942,7 +2943,10 @@ let rec setOneInit this o preinit =
let idx, (* Index in the current comp *)
restoff (* Rest offset *) =
match o with
- | Index({enode = Const(CInt64(i,_,_))}, off) -> to_integer i, off
+ | NoOffset -> assert false
+ | Index({enode = Const(CInt64(i,_,_));eloc}, off) ->
+ CurrentLoc.set eloc;
+ to_integer i, off
| Field (f, off) ->
(* Find the index of the field *)
let rec loop (idx: int) = function
@@ -2958,7 +2962,9 @@ let rec setOneInit this o preinit =
| _ :: restf -> loop (idx + 1) restf
in
loop 0 (Option.value ~default:[] f.fcomp.cfields), off
- | _ -> abort_context "setOneInit: non-constant index"
+ | Index({ eloc },_) ->
+ CurrentLoc.set eloc;
+ abort_context "setOneInit: non-constant index"
in
let pMaxIdx, pArray =
match this with
@@ -8337,6 +8343,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
end
| Cabs.ATINDEX_INIT(idx, whatnext) -> begin
+ CurrentLoc.set idx.expr_loc;
match unrollType so.soTyp with
| TArray (bt, leno, _) ->
let ilen = integerArrayLength leno in
diff --git a/tests/syntax/oracle/very_large_integers.13.res.oracle b/tests/syntax/oracle/very_large_integers.13.res.oracle
index baa5289f5572f4aa93d8eb04ac649a6b2bb3887d..e74ad25634d44e2274a374ae907cbca71e904c37 100644
--- a/tests/syntax/oracle/very_large_integers.13.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.13.res.oracle
@@ -9,7 +9,7 @@
100 #ifdef ARRAY_INIT1
101 // Previously caused Invalid_argument(Array.make)
102 int a1[] = {[72057594037927936] = 0};
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^
103 #endif
104
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.14.res.oracle b/tests/syntax/oracle/very_large_integers.14.res.oracle
index bfd5d8b7eb57423236a1136fb001b9e59c49351b..3ded691db128b079cba777fce10a9415a15903f9 100644
--- a/tests/syntax/oracle/very_large_integers.14.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.14.res.oracle
@@ -5,12 +5,12 @@
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:113: User Error:
+[kernel] very_large_integers.c:114: User Error:
array length too large: 7205759403792794
- 111 };
112 // Previously caused Out of memory
113 struct st s = {
- ^^^^^^^^^^^^^^^
114 {{[7205759403792793 ... 7205759403792793] = 0}}
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
115 };
+ 116 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.15.res.oracle b/tests/syntax/oracle/very_large_integers.15.res.oracle
index c8f36fffabbea0ea7fb9e8339e9582d4c8feefef..b39f7c8df96db714552373dbfb3e1964cff2bd78 100644
--- a/tests/syntax/oracle/very_large_integers.15.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.15.res.oracle
@@ -9,7 +9,7 @@
117
118 #ifdef ARRAY_INIT3
119 int ai3[] = {0xdead, [72057594037927936] = 0xbeef};
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^
120 #endif
121 #ifdef ARRAY_INIT4
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.16.res.oracle b/tests/syntax/oracle/very_large_integers.16.res.oracle
index 773cecaac1fd5f1a4faf437574f6578214519a23..eb45cfee5dbeda5a8364396ad9a361c61674cafc 100644
--- a/tests/syntax/oracle/very_large_integers.16.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.16.res.oracle
@@ -9,7 +9,7 @@
121 #ifdef ARRAY_INIT4
122 // Previously caused Out of memory
123 int ai4[] = {1, [7205759403792793] = 11};
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^
124 #endif
125
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.2.res.oracle b/tests/syntax/oracle/very_large_integers.2.res.oracle
index 999706dea413ac6c5c63956a666e93586569bb94..8fd8c4b251b674d680d7030fb0d834a073f4db09 100644
--- a/tests/syntax/oracle/very_large_integers.2.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.2.res.oracle
@@ -6,7 +6,7 @@
47 void case_range() {
48 switch (nondetul)
49 case 0 ... 9999999999999999999U:;
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
50 case 0 ... 199999999999999999U:;
51 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.3.res.oracle b/tests/syntax/oracle/very_large_integers.3.res.oracle
index 7c9ba7c178fdb4909990ec08bd4d6dcf11caf537..f36fb4343d810e2291e94fe870879b536f7a8698 100644
--- a/tests/syntax/oracle/very_large_integers.3.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.3.res.oracle
@@ -4,7 +4,7 @@
55 void case_range2() {
56 switch (nondet)
57 case 0 ... 10000000U:;
- ^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^
58 }
59 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.5.res.oracle b/tests/syntax/oracle/very_large_integers.5.res.oracle
index 2dd40615234abca06fe729a6f9805df6005aebe3..0e84fc8e48cfe064978ae9009f0990872c8857f9 100644
--- a/tests/syntax/oracle/very_large_integers.5.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.5.res.oracle
@@ -4,7 +4,7 @@
64
65 #ifdef INIT_DESIGNATOR2
66 int arr3[1] = { [9999999999999999999U] = 42 };
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^
67 #endif
68
[kernel] Frama-C aborted: invalid user input.