From bd5c857f345b3b7c031f5bda7444ba28fc15eb22 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 15 Dec 2020 09:18:14 +0100
Subject: [PATCH] [Kernel] more precise error message
---
src/kernel_services/ast_queries/logic_typing.ml | 2 +-
tests/spec/oracle/reset_env.res.oracle | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 22976eda684..2ea2ab6df82 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3163,7 +3163,7 @@ struct
with Not_found ->
C.find_all_logic_functions f in
match infos with
- | [] -> C.error loc "unbound function %s" f
+ | [] -> C.error loc "unbound logic function %s" f
| [info] ->
begin
let labels = List.map (find_logic_label loc env) labels in
diff --git a/tests/spec/oracle/reset_env.res.oracle b/tests/spec/oracle/reset_env.res.oracle
index 077d6e4aecb..88fafa445af 100644
--- a/tests/spec/oracle/reset_env.res.oracle
+++ b/tests/spec/oracle/reset_env.res.oracle
@@ -2,6 +2,6 @@
[kernel:annot-error] tests/spec/reset_env.i:5: Warning:
unbound logic variable INEXISTENT_SYMBOL. Ignoring global annotation
[kernel:annot-error] tests/spec/reset_env.i:9: Warning:
- unbound function bla. Ignoring specification of function f
+ unbound logic function bla. Ignoring specification of function f
/* Generated by Frama-C */
--
GitLab