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

[eacsl] Remove `-variadic-no-translation` when calling E-ACSL

parent b1ecbcfb
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+ 1
− 2
View file @ df56487d
...@@ -763,8 +763,7 @@ LDFLAGS="$OPTION_LDFLAGS" ...@@ -763,8 +763,7 @@ LDFLAGS="$OPTION_LDFLAGS"
# Extra Frama-C Flags E-ACSL needs # Extra Frama-C Flags E-ACSL needs
FRAMAC_FLAGS="$FRAMAC_FLAGS \ FRAMAC_FLAGS="$FRAMAC_FLAGS \
-remove-unused-specified-functions \ -remove-unused-specified-functions"
-variadic-no-translation"
# C, CPP and LD flags for compilation of E-ACSL-generated sources # C, CPP and LD flags for compilation of E-ACSL-generated sources
EACSL_CFLAGS="$OPTION_EXTERNAL_ASSERT" EACSL_CFLAGS="$OPTION_EXTERNAL_ASSERT"
......
src/plugins/e-acsl/tests/test_config_ci.in
+ 1
− 1
View file @ df56487d
MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@ MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
MACRO: MACHDEP -machdep gcc_x86_64 MACRO: MACHDEP -machdep gcc_x86_64
MACRO: GLOBAL @MACHDEP@ -remove-unused-specified-functions -variadic-no-translation -verbose 0 MACRO: GLOBAL @MACHDEP@ -remove-unused-specified-functions -verbose 0
MACRO: EACSL -e-acsl -e-acsl-share ./share/e-acsl -e-acsl-verbose 1 MACRO: EACSL -e-acsl -e-acsl-share ./share/e-acsl -e-acsl-verbose 1
MACRO: EVA -eva -eva-no-alloc-returns-null -eva-no-results -eva-no-print -eva-warn-key libc:unsupported-spec=inactive MACRO: EVA -eva -eva-no-alloc-returns-null -eva-no-results -eva-no-print -eva-warn-key libc:unsupported-spec=inactive
MACRO: EVENTUALLY -print -ocode @DEST@.c -load-script ./tests/print.cmxs MACRO: EVENTUALLY -print -ocode @DEST@.c -load-script ./tests/print.cmxs
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment