From 886896546c211fb4e4db7832208bddc8454c6825 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 28 Mar 2023 12:38:54 +0200
Subject: [PATCH] [Eva] Values request: fixes evaluation of uninitialized or
escaping lvalues.
---
src/plugins/eva/api/values_request.ml | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index 7a547dec352..e6a33b7f6ad 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -403,17 +403,17 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
(* Result of an evaluation: a generic value for scalar types, or an offsetmap
for struct and arrays. *)
type result =
- | Value of A.Val.t
+ | Value of A.Val.t Eval.flagged_value
| Offsetmap of offsetmap
| Status of truth
let pp_result typ fmt = function
- | Value v -> A.Val.pretty fmt v
+ | Value v -> (Eval.Flagged_Value.pretty (A.Val.pretty_typ (Some typ))) fmt v
| Offsetmap offsm -> pp_offsetmap typ fmt offsm
| Status truth -> Alarmset.Status.pretty fmt truth
let get_pointed_bases = function
- | Value v -> get_bases (get_cvalue v)
+ | Value v -> get_bases (Bottom.fold ~bottom:Cvalue.V.bottom get_cvalue v.v)
| Offsetmap offsm -> get_pointed_bases offsm
| Status _ -> Base.Hptset.empty
@@ -460,13 +460,13 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let eval_lval lval state =
match Cil.(unrollType (typeOfLval lval)) with
| TInt _ | TEnum _ | TPtr _ | TFloat _ ->
- A.copy_lvalue state lval >>=. fun value ->
- value.v >>-: fun v -> Value v
+ A.copy_lvalue state lval >>=: fun value -> Value value
| _ ->
lval_to_offsetmap lval state >>=: fun offsm -> Offsetmap offsm
let eval_expr expr state =
- A.eval_expr state expr >>=: fun value -> Value value
+ A.eval_expr state expr >>=: fun value ->
+ Value { v = `Value value; initialized = true; escaping = false }
let eval_pred eval_point predicate state =
let result =
--
GitLab