From 663b963b8bec6385c8918e49fc8692c73f665983 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 8 Jan 2024 15:11:33 +0100
Subject: [PATCH] [eva] fix sparse sets & unspecified seq.
---
src/plugins/eva/utils/annot.ml | 23 ++++++++++++-----------
1 file changed, 12 insertions(+), 11 deletions(-)
diff --git a/src/plugins/eva/utils/annot.ml b/src/plugins/eva/utils/annot.ml
index 219dce96d16..f7b5c6f5f4e 100644
--- a/src/plugins/eva/utils/annot.ml
+++ b/src/plugins/eva/utils/annot.ml
@@ -97,17 +97,18 @@ let imax (exp : Exp.exp) (ival : Ival.t) : pred =
| None -> True
| Some k -> Eval Exp.( exp <= of_integer k )
-let irange = function
- | [_] | [] -> false
+let sparse = function
+ | [] -> false
+ | [_] -> true
| x::xs ->
let rec continuous x = function
| [] -> true
| y::ys -> Z.equal (Z.succ x) y && continuous y ys
- in continuous x xs
+ in not @@ continuous x xs
let ival (exp : Exp.exp) (ival : Ival.t) : pred =
match Ival.project_small_set ival with
- | Some vs when not @@ irange vs ->
+ | Some vs when sparse vs ->
List.fold_left (fun w v -> por w (iequal exp v)) False vs
| _ -> pand (imin exp ival) (imax exp ival)
@@ -231,14 +232,14 @@ class evaluator request =
method !vstmt_aux stmt =
match stmt.skind with
- (* Branching expressions *)
- | If(e,_,_,_) | Switch(e,_,_,_) ->
- self#visit_expr e ; SkipChildren
(* Instructions *)
- | Instr _ | Return _ | Goto _ | Break _ | Continue _
- | UnspecifiedSequence _ -> DoChildren
- (* Blocks *)
- | Loop _ | Block _ | Throw _ | TryCatch _ | TryFinally _ | TryExcept _
+ | Instr _ | Return _ -> DoChildren
+ (* Branching expressions *)
+ | If(e,_,_,_) | Switch(e,_,_,_) -> self#visit_expr e ; SkipChildren
+ (* Blocks & Jumps *)
+ | Goto _ | Break _ | Continue _
+ | Loop _ | Block _ | UnspecifiedSequence _
+ | Throw _ | TryCatch _ | TryFinally _ | TryExcept _
-> SkipChildren
end
--
GitLab