From ac88b4ba6e3372b04d241f2e060ff79530c09d38 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 18 Feb 2021 08:52:36 +0100
Subject: [PATCH] [logic] refine duplicate lemma error message
---
src/kernel_services/ast_queries/logic_typing.ml | 9 +++++++--
tests/spec/oracle/axiom_redef_bts1005.res.oracle | 2 +-
2 files changed, 8 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index ca5511407cf..1789b851855 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -4191,9 +4191,14 @@ struct
| LDlemma (x,labels, poly, {tp_kind = kind; tp_statement = e}) ->
if Logic_env.Lemmas.mem x then begin
let old_def = Logic_env.Lemmas.find x in
+ let old_kind = match old_def with
+ | Dlemma(_,_,_,{tp_kind },_,_) -> tp_kind
+ | _ -> Assert in
let old_loc = Cil_datatype.Global_annotation.loc old_def in
- C.error loc "lemma %s is already registered (%a)"
- x Cil_datatype.Location.pretty old_loc
+ C.error loc "%a %s is already registered as %a (%a)"
+ Cil_printer.pp_lemma_kind kind x
+ Cil_printer.pp_lemma_kind old_kind
+ Cil_datatype.Location.pretty old_loc
end;
let labels,env = annot_env loc labels poly in
let p = Logic_const.toplevel_predicate ~kind (predicate env e) in
diff --git a/tests/spec/oracle/axiom_redef_bts1005.res.oracle b/tests/spec/oracle/axiom_redef_bts1005.res.oracle
index d6bf2400ede..01b443473c6 100644
--- a/tests/spec/oracle/axiom_redef_bts1005.res.oracle
+++ b/tests/spec/oracle/axiom_redef_bts1005.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/spec/axiom_redef_bts1005.i (no preprocessing)
[kernel:annot-error] tests/spec/axiom_redef_bts1005.i:5: Warning:
- lemma inj1 is already registered (tests/spec/axiom_redef_bts1005.i:4). Ignoring global annotation
+ axiom inj1 is already registered as axiom (tests/spec/axiom_redef_bts1005.i:4). Ignoring global annotation
/* Generated by Frama-C */
--
GitLab