Skip to content
Snippets Groups Projects
Commit bd5c857f authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[Kernel] more precise error message

parent b3994d11
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/kernel_services/ast_queries/logic_typing.ml
+ 1
− 1
View file @ bd5c857f
...@@ -3163,7 +3163,7 @@ struct ...@@ -3163,7 +3163,7 @@ struct
with Not_found -> with Not_found ->
C.find_all_logic_functions f in C.find_all_logic_functions f in
match infos with match infos with
| [] -> C.error loc "unbound function %s" f | [] -> C.error loc "unbound logic function %s" f
| [info] -> | [info] ->
begin begin
let labels = List.map (find_logic_label loc env) labels in let labels = List.map (find_logic_label loc env) labels in
......
tests/spec/oracle/reset_env.res.oracle
+ 1
− 1
View file @ bd5c857f
...@@ -2,6 +2,6 @@ ...@@ -2,6 +2,6 @@
[kernel:annot-error] tests/spec/reset_env.i:5: Warning: [kernel:annot-error] tests/spec/reset_env.i:5: Warning:
unbound logic variable INEXISTENT_SYMBOL. Ignoring global annotation unbound logic variable INEXISTENT_SYMBOL. Ignoring global annotation
[kernel:annot-error] tests/spec/reset_env.i:9: Warning: [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 */ /* Generated by Frama-C */
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment