From 9c42846dfc438b036de8dd516a54afd8ec914fa5 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 24 Jan 2024 17:36:38 +0100
Subject: [PATCH] [kernel] better localisation for error msgs on array indices
---
src/kernel_internals/typing/cabs2cil.ml | 15 +++++++++++----
.../oracle/very_large_integers.13.res.oracle | 2 +-
.../oracle/very_large_integers.14.res.oracle | 6 +++---
.../oracle/very_large_integers.15.res.oracle | 2 +-
.../oracle/very_large_integers.16.res.oracle | 2 +-
.../oracle/very_large_integers.2.res.oracle | 2 +-
.../oracle/very_large_integers.3.res.oracle | 2 +-
.../oracle/very_large_integers.5.res.oracle | 2 +-
8 files changed, 20 insertions(+), 13 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index c440701e41c..d98f976c738 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 baa5289f557..e74ad25634d 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 bfd5d8b7eb5..3ded691db12 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 c8f36fffabb..b39f7c8df96 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 773cecaac1f..eb45cfee5db 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 999706dea41..8fd8c4b251b 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 7c9ba7c178f..f36fb4343d8 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 2dd40615234..0e84fc8e48c 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.
--
GitLab