From b46b09b7cacd3ba4bbf0d33b133356624304f784 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 25 Jan 2024 18:47:31 +0100
Subject: [PATCH] [kernel] Better localization for cast errors
---
src/kernel_services/ast_queries/cil.ml | 4 ++--
tests/syntax/oracle/array_cast_bts1099.res.oracle | 2 +-
tests/syntax/oracle/wrong-assignment.res.oracle | 2 +-
3 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 6bfd4b301b5..2ff3b6f2789 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -71,10 +71,10 @@ let () = Log.set_current_source (fun () -> fst (CurrentLoc.get ()))
let pp_thisloc fmt = Location.pretty fmt (CurrentLoc.get ())
let abort_context msg =
- let pos = fst (CurrentLoc.get ()) in
+ let (start_pos,pos) = CurrentLoc.get () in
let append fmt =
Format.pp_print_newline fmt ();
- Errorloc.pp_context_from_file fmt pos
+ Errorloc.pp_context_from_file ~start_pos fmt pos
in
Kernel.abort ~current:true ~append msg
diff --git a/tests/syntax/oracle/array_cast_bts1099.res.oracle b/tests/syntax/oracle/array_cast_bts1099.res.oracle
index 09ba17a47e2..9ba1eb0a363 100644
--- a/tests/syntax/oracle/array_cast_bts1099.res.oracle
+++ b/tests/syntax/oracle/array_cast_bts1099.res.oracle
@@ -4,6 +4,6 @@
10 int tab1[4];
11 u* p = &tab1;
12 t* p2 = (t) p;
- ^^^^^^^^^^^^^^^^
+ ^^^^^
13 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/wrong-assignment.res.oracle b/tests/syntax/oracle/wrong-assignment.res.oracle
index a6f9c43d92d..2dd3d505f17 100644
--- a/tests/syntax/oracle/wrong-assignment.res.oracle
+++ b/tests/syntax/oracle/wrong-assignment.res.oracle
@@ -4,6 +4,6 @@
11 void d() {
12 // this assignment should be rejected
13 c.a = b;
- ^^^^^^^^^^
+ ^
14 }
[kernel] Frama-C aborted: invalid user input.
--
GitLab