From 60215bfc5278aa6148a7c8b7b9810da1c9c097f5 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 25 Jan 2024 14:52:40 +0100
Subject: [PATCH] [kernel] Fix CurrentLoc when doing index range inits checks
---
src/kernel_internals/typing/cabs2cil.ml | 1 +
tests/syntax/oracle/very_large_integers.6.res.oracle | 2 +-
tests/syntax/oracle/very_large_integers.7.res.oracle | 2 +-
3 files changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4e13f8455dd..3925038637d 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 8858cc405bb..a276df46d02 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 22ddabcd753..9e0b1da102e 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.
--
GitLab