From 0c3459c44e45c39c609acdf409d18ccda98c1960 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 8 Jan 2024 16:03:56 +0100
Subject: [PATCH] [eva] refrain from annotating further unreachable statements
---
src/plugins/eva/utils/annot.ml | 31 +++++++++++++--------
tests/misc/eva_annot_dead.c | 9 ++++--
tests/misc/oracle/eva_annot_dead.res.oracle | 19 +++++--------
3 files changed, 33 insertions(+), 26 deletions(-)
diff --git a/src/plugins/eva/utils/annot.ml b/src/plugins/eva/utils/annot.ml
index 13668d81949..dee838d019a 100644
--- a/src/plugins/eva/utils/annot.ml
+++ b/src/plugins/eva/utils/annot.ml
@@ -27,6 +27,7 @@ open Cil_types
(* -------------------------------------------------------------------------- *)
module Ltype = Cil_datatype.Logic_type_ByName
+module Stmts = Cil_datatype.Stmt.Set
module Exp = Cil_builder.Exp
type visitor = Visitor.frama_c_visitor
@@ -270,6 +271,7 @@ let generated = Emitter.create "Eva_domain"
class generator =
object(self)
inherit Visitor.frama_c_inplace
+ val mutable dead = Stmts.empty (* annotated as dead *)
method! vlval _ = SkipChildren
method! vexpr _ = SkipChildren
@@ -278,18 +280,23 @@ class generator =
match self#current_kf with
| None -> Cil.SkipChildren
| Some kf ->
- List.iter
- (Annotations.add_assert generated ~kf stmt)
- (eval_instr stmt) ;
- Annotations.iter_code_annot
- (fun e ca ->
- if Emitter.equal e generated then
- List.iter
- (fun ip ->
- Property_status.emit Analysis.emitter ~hyps:[] ip True
- ) (Property.ip_of_code_annot kf stmt ca)
- ) stmt ;
- if is_dead stmt then SkipChildren else DoChildren
+ if not @@ List.for_all (fun s -> Stmts.mem s dead) stmt.preds then
+ begin
+ List.iter
+ (Annotations.add_assert generated ~kf stmt)
+ (eval_instr stmt) ;
+ Annotations.iter_code_annot
+ (fun e ca ->
+ if Emitter.equal e generated then
+ List.iter
+ (fun ip ->
+ Property_status.emit Analysis.emitter ~hyps:[] ip True
+ ) (Property.ip_of_code_annot kf stmt ca)
+ ) stmt ;
+ end ;
+ if is_dead stmt
+ then ( dead <- Stmts.add stmt dead ; SkipChildren )
+ else DoChildren
end
diff --git a/tests/misc/eva_annot_dead.c b/tests/misc/eva_annot_dead.c
index 3124bc93bb6..3cf2a4d788b 100644
--- a/tests/misc/eva_annot_dead.c
+++ b/tests/misc/eva_annot_dead.c
@@ -9,8 +9,13 @@
int main(int a) {
int b = 0;
- if (a < 0) { a = 1; b++; }
- if (a < 0) { a = 2; b++; }
+ if (a) goto B;
+ if (0) {
+ b++;
+ b++;
+ B:
+ b += 42;
+ }
return b;
}
diff --git a/tests/misc/oracle/eva_annot_dead.res.oracle b/tests/misc/oracle/eva_annot_dead.res.oracle
index 6e682969acd..62caab0d8d3 100644
--- a/tests/misc/oracle/eva_annot_dead.res.oracle
+++ b/tests/misc/oracle/eva_annot_dead.res.oracle
@@ -4,8 +4,7 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
- a ∈ [0..2147483647]
- b ∈ {0; 1}
+ b ∈ {0; 42}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
1 function analyzed (out of 1): 100% coverage.
@@ -23,19 +22,15 @@ int main(int a)
{
int b = 0;
/*@ assert Eva_domain: -2147483648 ≤ a ≤ 2147483647; */
- if (a < 0) {
- a = 1;
- /*@ assert Eva_domain: b ≡ 0; */
- b ++;
- }
- /*@ assert Eva_domain: 0 ≤ a ≤ 2147483647; */
- if (a < 0) {
- /*@ assert Eva_domain: \false; */
- a = 2;
+ if (a) goto B;
+ if (0) {
/*@ assert Eva_domain: \false; */
b ++;
+ b ++;
+ B: /*@ assert Eva_domain: b ≡ 0; */
+ b += 42;
}
- /*@ assert Eva_domain: 0 ≤ b ≤ 1; */
+ /*@ assert Eva_domain: b ≡ 0 ∨ b ≡ 42; */
return b;
}
--
GitLab