From 1cfe295d2298c83edc1cce57e26c586f15b802a2 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 6 Apr 2021 15:28:58 +0200
Subject: [PATCH] [Eva] Fix a bug where added annotations were always slevel
annotations
---
src/plugins/value/utils/eva_annotations.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index e17f1d03ffd..4d019227478 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -99,7 +99,7 @@ struct
let add ~emitter ~loc stmt annot =
let param = M.export annot in
- let extension = Logic_const.new_acsl_extension "slevel" loc false param in
+ let extension = Logic_const.new_acsl_extension name loc false param in
let annot_node = Cil_types.AExtended ([], false, extension) in
let code_annotation = Logic_const.new_code_annotation annot_node in
Annotations.add_code_annot emitter stmt code_annotation
--
GitLab