From 42a86155f0d5487fda98559f6a88a24016218e59 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 9 Mar 2021 17:09:08 +0100
Subject: [PATCH] [eacsl] Add Variant annotation kind
---
src/plugins/e-acsl/src/code_generator/smart_stmt.ml | 2 ++
src/plugins/e-acsl/src/code_generator/smart_stmt.mli | 1 +
2 files changed, 3 insertions(+)
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
index 1cc37e8113c..9799cadb813 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
@@ -44,6 +44,7 @@ type annotation_kind =
| Precondition
| Postcondition
| Invariant
+ | Variant
| RTE
let kind_to_string loc k =
@@ -54,6 +55,7 @@ let kind_to_string loc k =
| Precondition -> "Precondition"
| Postcondition -> "Postcondition"
| Invariant -> "Invariant"
+ | Variant -> "Variant"
| RTE -> "RTE")
let block stmt b = match b.bstmts with
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
index c56404a5a71..4cdeb0fd23d 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
@@ -104,6 +104,7 @@ type annotation_kind =
| Precondition
| Postcondition
| Invariant
+ | Variant
| RTE
val runtime_check:
--
GitLab