Skip to content
Snippets Groups Projects
Commit b1ecbcfb authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Variadic translation is incompatible with `-e-acsl-validate-format-string`

parent ba25aa73
No related branches found
No related tags found
No related merge requests found
...@@ -42,12 +42,14 @@ let generate_code = ...@@ -42,12 +42,14 @@ let generate_code =
Temporal.enable (Options.Temporal_validity.get ()); Temporal.enable (Options.Temporal_validity.get ());
if Plugin.is_present "variadic" then begin if Plugin.is_present "variadic" then begin
let opt_name = "-variadic-translation" in 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 if Ast.is_computed () then
Options.abort Options.abort
"The variadic translation must be turned off for E-ACSL. \ "The variadic translation is incompatible with E-ACSL option \
Please use option '-variadic-no-translation'"; '%s'.@ Please use option '-variadic-no-translation'."
Options.warning "deactivating variadic translation"; Options.Validate_format_strings.option_name
Options.warning "deactivating variadic translation";
Dynamic.Parameter.Bool.off opt_name (); Dynamic.Parameter.Bool.off opt_name ();
end end
end; end;
......
STDOPT: #"-e-acsl-validate-format-strings" STDOPT: #"-variadic-no-translation -e-acsl-validate-format-strings"
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|" MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e "s|/.*/share/e-acsl|FRAMAC_SHARE/e-acsl|"
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment