From 048ce8fde361db1bb5dd34ee64142f8e7efcd61f Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 26 Mar 2014 18:51:48 +0100
Subject: [PATCH] fix bug #1692 about wrong localisation of messages emitted
when typing
---
src/plugins/e-acsl/doc/Changelog | 2 ++
src/plugins/e-acsl/typing.ml | 6 +++++-
2 files changed, 7 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 9d22701682e..f16e51a4b5f 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2014/03/26] Fix bug #1692 about wrong localisation of
+ some messages.
- E-ACSL [2014/03/26] Remove a spurious warning when an annotated
function is first declared, then defined.
-* E-ACSL [2014/03/25] Fix bug #1716 with annotations in while(1).
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index dee58a68684..a1a41887cdc 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -164,6 +164,7 @@ module Term_env = Make_env(Term)(struct type t = eacsl_typ * eacsl_typ end)
module Logic_var_env = Make_env(Logic_var)(struct type t = eacsl_typ end)
let generic_typ (which: < f: 'a. 'a * 'a -> 'a >) t =
+ Cil.CurrentLoc.set t.term_loc;
if Options.Gmp_only.get () then
let ty = match t.term_type with
| Linteger -> Mpz.t ()
@@ -241,6 +242,7 @@ let type_of_indexed_host = function
| _ -> assert false
let rec type_term t =
+ Cil.CurrentLoc.set t.term_loc;
let lty = t.term_type in
let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
let dup f x = let y = f x in y, y in
@@ -440,7 +442,9 @@ let compute_quantif_guards_ref
(term * relation * logic_var * relation * term) list) ref
= Extlib.mk_fun "compute_quantif_guards_ref"
-let rec type_predicate_named p = match p.content with
+let rec type_predicate_named p =
+ Cil.CurrentLoc.set p.loc;
+ match p.content with
| Pfalse | Ptrue -> ()
| Papp _ -> Error.not_yet "logic function application"
| Pseparated _ -> Error.not_yet "\\separated"
--
GitLab