From e13e0ae61ddff4dc016c30600ce9f91118f67e9f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 13 Nov 2020 12:38:59 +0100
Subject: [PATCH] [Eva] Uses constants in bitwise AND operations as widening
thresholds.
---
src/plugins/value/utils/widen.ml | 32 ++++++++++++++++++--------------
1 file changed, 18 insertions(+), 14 deletions(-)
diff --git a/src/plugins/value/utils/widen.ml b/src/plugins/value/utils/widen.ml
index fd0ba303f42..dd9dd003437 100644
--- a/src/plugins/value/utils/widen.ml
+++ b/src/plugins/value/utils/widen.ml
@@ -172,20 +172,24 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
List.iter aux_loop enclosing_loops;
Cil.DoChildren
end
- | Instr (Set ((Var vi, _), exp, _) ) -> begin
- match exp.enode with
- | BinOp (Mod, _, modu, _typ)
- | CastE (_typ, {enode = BinOp (Mod, _, modu, _)}) ->
- begin
- match Cil.constFoldToInt modu with
- | None -> ()
- | Some i ->
- let base = Base.of_varinfo vi in
- let threshold = Ival.Widen_Hints.singleton (Integer.pred i) in
- self#add_int_thresholds ~base threshold;
- end
- | _ -> ()
- end;
+ | Instr (Set ((Var vi, _), exp, _) ) ->
+ let rec find_candidates expr =
+ match expr.enode with
+ | BinOp (Mod, _, modu, _typ) -> [modu]
+ | BinOp (LAnd, e1, e2, _typ) -> [e1; e2]
+ | CastE (_, expr)
+ | Info (expr, _) -> find_candidates expr
+ | _ -> []
+ in
+ let process expr =
+ match Cil.constFoldToInt expr with
+ | None -> ()
+ | Some i ->
+ let base = Base.of_varinfo vi in
+ let threshold = Ival.Widen_Hints.singleton (Integer.pred i) in
+ self#add_int_thresholds ~base threshold
+ in
+ List.iter process (find_candidates exp);
Cil.DoChildren
| _ -> Cil.DoChildren
--
GitLab