From 841e4fbc24af65f7a1d4c4baa74ceba2d3dc384b Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 1 Feb 2024 18:48:51 +0100
Subject: [PATCH] Fix aorai CurrentLoc
---
src/plugins/aorai/aorai_dataflow.ml | 2 ++
src/plugins/aorai/tests/ya/oracle/monostate.res.oracle | 2 +-
2 files changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index b44b715ecd4..b569d4c464a 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -962,6 +962,8 @@ let filter_init_state restrict initial map acc =
with Not_found -> acc
let backward_analysis_aux stack kf ret_state =
+ let open Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = Kernel_function.get_location kf in
if Data_for_aorai.isIgnoredFunction kf then
Aorai_option.fatal
"Call backward analysis on ignored function %a" Kernel_function.pretty kf
diff --git a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
index ec532e72681..3d2eb83f556 100644
--- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing monostate.i (no preprocessing)
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[aorai] monostate.i:10: Warning:
+[aorai] monostate.i:9: Warning:
Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path
[kernel] Parsing TMPDIR/aorai_monostate_0.i (no preprocessing)
/* Generated by Frama-C */
--
GitLab