From b1ecbcfbd86efe72e65c272465e9f060270bb796 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 9 Oct 2020 15:59:55 +0200
Subject: [PATCH] [eacsl] Variadic translation is incompatible with
`-e-acsl-validate-format-string`
---
src/plugins/e-acsl/src/main.ml | 10 ++++++----
src/plugins/e-acsl/tests/format/test_config_ci | 2 +-
src/plugins/e-acsl/tests/format/test_config_dev | 2 +-
3 files changed, 8 insertions(+), 6 deletions(-)
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 8de1804974e..8439a6b2b72 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -42,12 +42,14 @@ let generate_code =
Temporal.enable (Options.Temporal_validity.get ());
if Plugin.is_present "variadic" then begin
let opt_name = "-variadic-translation" in
- if Dynamic.Parameter.Bool.get opt_name () then begin
+ if Dynamic.Parameter.Bool.get opt_name () &&
+ Options.Validate_format_strings.get () then begin
if Ast.is_computed () then
Options.abort
- "The variadic translation must be turned off for E-ACSL. \
- Please use option '-variadic-no-translation'";
- Options.warning "deactivating variadic translation";
+ "The variadic translation is incompatible with E-ACSL option \
+ '%s'.@ Please use option '-variadic-no-translation'."
+ Options.Validate_format_strings.option_name
+ Options.warning "deactivating variadic translation";
Dynamic.Parameter.Bool.off opt_name ();
end
end;
diff --git a/src/plugins/e-acsl/tests/format/test_config_ci b/src/plugins/e-acsl/tests/format/test_config_ci
index eeaea353f8a..982e648c83f 100644
--- a/src/plugins/e-acsl/tests/format/test_config_ci
+++ b/src/plugins/e-acsl/tests/format/test_config_ci
@@ -1 +1 @@
-STDOPT: #"-e-acsl-validate-format-strings"
+STDOPT: #"-variadic-no-translation -e-acsl-validate-format-strings"
diff --git a/src/plugins/e-acsl/tests/format/test_config_dev b/src/plugins/e-acsl/tests/format/test_config_dev
index 636b97b9214..aae787763c6 100644
--- a/src/plugins/e-acsl/tests/format/test_config_dev
+++ b/src/plugins/e-acsl/tests/format/test_config_dev
@@ -1,2 +1,2 @@
-MACRO: ROOT_EACSL_GCC_OPTS_EXT --validate-format-strings --full-mtracking
+MACRO: ROOT_EACSL_GCC_OPTS_EXT --validate-format-strings --full-mtracking -F -variadic-no-translation
MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e "s|/.*/share/e-acsl|FRAMAC_SHARE/e-acsl|"
--
GitLab