Skip to content
Snippets Groups Projects
Commit 9993ef8b authored by David Bühler's avatar David Bühler
Browse files

[Eva] Frama_C_show_* directives do not impact the automatic loop unrolling.

parent 3751a20d
No related branches found
No related tags found
No related merge requests found
...@@ -77,6 +77,11 @@ let find_loop_exit_condition loop = ...@@ -77,6 +77,11 @@ let find_loop_exit_condition loop =
in in
aux loop.bstmts aux loop.bstmts
let is_frama_c_builtin exp =
match exp.enode with
| Lval (Var vi, NoOffset) -> Ast_info.is_frama_c_builtin vi.vname
| _ -> false
(* Effects of a loop: (* Effects of a loop:
- set of varinfos that are directly modified within the loop. Pointer - set of varinfos that are directly modified within the loop. Pointer
accesses are ignored. accesses are ignored.
...@@ -111,7 +116,7 @@ let loop_effect_visitor = object (self) ...@@ -111,7 +116,7 @@ let loop_effect_visitor = object (self)
in in
let () = match instr with let () = match instr with
| Asm _ -> assembly <- true | Asm _ -> assembly <- true
| Call _ -> call <- true | Call (_, exp, _, _) when not (is_frama_c_builtin exp) -> call <- true
| _ -> () | _ -> ()
in in
Cil.SkipChildren Cil.SkipChildren
......
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