From 3faeacad914d31d60eecdac31ebd885898114bfc Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 12 Jan 2021 10:27:07 +0100
Subject: [PATCH] [aorai] warns if an observable of the automaton is not
defined (hence ignored).
---
src/plugins/aorai/data_for_aorai.ml | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index b333a7531da..b3da1ce5c06 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -1579,7 +1579,12 @@ let check_observables auto =
| Some set ->
let is_relevant name =
try
- ignore (Globals.Functions.find_by_name name)
+ let kf = Globals.Functions.find_by_name name in
+ if not (Kernel_function.is_definition kf) then
+ Aorai_option.warning
+ "Function %a is observable by the automaton but is not defined \
+ in the C code. It will be ignored in the instrumentation"
+ Printer.pp_varname (Kernel_function.get_name kf)
with Not_found ->
Aorai_option.abort "Observable %s doesn't match any function" name
in
--
GitLab