From 20e6773d376b57d7c7f0ad893cdc5f8925442a78 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 2 May 2023 14:07:28 +0200
Subject: [PATCH] [Eva] Octagons: do not infer relations or intervals on global
initializations.
Fixes performance issues: the initialization of large arrays or structures
can lead to a very large number of relations or intervals.
Also, do not infer intervals on volatile lvalues.
---
src/plugins/eva/domains/octagons.ml | 10 ++++++----
1 file changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index 250832bcdcd..f547c7da3ce 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -1627,7 +1627,6 @@ module Domain = struct
in
eval_exp, eval_deps
-
(* Domain functions *)
let extract_expr ~oracle _context state expr =
@@ -1708,7 +1707,8 @@ module Domain = struct
then state
else
match expr.enode with
- | Lval lval when Cil.(isIntegralType (typeOfLval lval)) ->
+ | Lval lval when Cil.(isIntegralType (typeOfLval lval))
+ && not (Eval_typ.lval_contains_volatile lval) ->
let var = Variable.make_lval lval in
let deps = Deps.add var (eval_deps var) state.deps in
let intervals = Intervals.add var ival state.intervals in
@@ -1788,9 +1788,11 @@ module Domain = struct
in
state >>-: check "precise assign"
- let assign _kinstr left_value expr assigned valuation state =
+ let assign kinstr left_value expr assigned valuation state =
update valuation state >>- fun state ->
- if Cil.isIntegralOrPointerType left_value.ltyp
+ if kinstr <> Kglobal
+ && Cil.isIntegralOrPointerType left_value.ltyp
+ && not (Eval_typ.lval_contains_volatile left_value.lval)
then assign_variable left_value.lval expr assigned valuation state
else
let written_loc = Precise_locs.imprecise_location left_value.lloc in
--
GitLab