Skip to content
Snippets Groups Projects
Commit 841e4fbc authored by Thibault Martin's avatar Thibault Martin Committed by Virgile Prevosto
Browse files

Fix aorai CurrentLoc

parent a7b40a45
No related branches found
No related tags found
No related merge requests found
...@@ -962,6 +962,8 @@ let filter_init_state restrict initial map acc = ...@@ -962,6 +962,8 @@ let filter_init_state restrict initial map acc =
with Not_found -> acc with Not_found -> acc
let backward_analysis_aux stack kf ret_state = 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 if Data_for_aorai.isIgnoredFunction kf then
Aorai_option.fatal Aorai_option.fatal
"Call backward analysis on ignored function %a" Kernel_function.pretty kf "Call backward analysis on ignored function %a" Kernel_function.pretty kf
......
[kernel] Parsing monostate.i (no preprocessing) [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] 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 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) [kernel] Parsing TMPDIR/aorai_monostate_0.i (no preprocessing)
/* Generated by Frama-C */ /* Generated by Frama-C */
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment