From abd17210b0cbcac936a75fb8edd129f4561eb6b7 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 30 Mar 2021 17:43:44 +0200
Subject: [PATCH] [eacsl] Fix "not yet" message for decreases clauses
---
src/plugins/e-acsl/src/code_generator/translate_annots.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
index 2046b2b4bed..d337b04075c 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -57,7 +57,7 @@ let pre_funspec kf kinstr env funspec =
unsupported
(fun spec ->
let ppt = Property.ip_decreases_of_spec kf kinstr spec in
- if must_translate_opt ppt then Env.not_yet env "variant clause")
+ if must_translate_opt ppt then Env.not_yet env "decreases clause")
funspec;
(* TODO: spec.spec_terminates is not part of the E-ACSL subset *)
unsupported
--
GitLab