diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml index 22976eda684e7727cf4c2654033a74713154da54..2ea2ab6df824ed0be52537143ac8cf2c5634a23f 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 077d6e4aecb1dc5a9fdd18d7e1974df4abfc8d61..88fafa445afe2bfb59aa287f073c5ca346586f4e 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 */