From 9993ef8bbf22e964e9dd8792cd6c7c6e006e4a13 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Tue, 7 Jul 2020 08:43:39 +0200 Subject: [PATCH] [Eva] Frama_C_show_* directives do not impact the automatic loop unrolling. --- src/plugins/value/partitioning/auto_loop_unroll.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml index c012563e68e..7b3c51f5b62 100644 --- a/src/plugins/value/partitioning/auto_loop_unroll.ml +++ b/src/plugins/value/partitioning/auto_loop_unroll.ml @@ -77,6 +77,11 @@ let find_loop_exit_condition loop = in 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: - set of varinfos that are directly modified within the loop. Pointer accesses are ignored. @@ -111,7 +116,7 @@ let loop_effect_visitor = object (self) in let () = match instr with | Asm _ -> assembly <- true - | Call _ -> call <- true + | Call (_, exp, _, _) when not (is_frama_c_builtin exp) -> call <- true | _ -> () in Cil.SkipChildren -- GitLab