Skip to content
Snippets Groups Projects
Commit 48d50dd9 authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl:e-acsl-gcc.sh] add new option --then-last

parent 2982a4bf
No related branches found
No related tags found
No related merge requests found
...@@ -340,7 +340,7 @@ LONGOPTIONS="help,compile,compile-only,debug:,ocode:,oexec:,verbose:, ...@@ -340,7 +340,7 @@ LONGOPTIONS="help,compile,compile-only,debug:,ocode:,oexec:,verbose:,
frama-c-only,extra-cpp-args:,frama-c-stdlib,full-mmodel,full-mtracking,gmp, frama-c-only,extra-cpp-args:,frama-c-stdlib,full-mmodel,full-mtracking,gmp,
quiet,logfile:,ld-flags:,cpp-flags:,frama-c-extra:,memory-model:,keep-going, quiet,logfile:,ld-flags:,cpp-flags:,frama-c-extra:,memory-model:,keep-going,
frama-c:,gcc:,e-acsl-share:,instrumented-only,rte:,oexec-e-acsl:,concurrency, frama-c:,gcc:,e-acsl-share:,instrumented-only,rte:,oexec-e-acsl:,concurrency,
print-mmodels,rt-debug,rte-select:,then,e-acsl-extra:,check,fail-with-code:, print-mmodels,rt-debug,rte-select:,then,then-last,e-acsl-extra:,check,fail-with-code:,
temporal,weak-validity,stack-size:,heap-size:,zone-sizes:,rt-verbose, temporal,weak-validity,stack-size:,heap-size:,zone-sizes:,rt-verbose,
free-valid-address,external-assert:,assert-print-data,no-assert-print-data, free-valid-address,external-assert:,assert-print-data,no-assert-print-data,
external-print-value:,validate-format-strings,no-trace,libc-replacements, external-print-value:,validate-format-strings,no-trace,libc-replacements,
...@@ -388,7 +388,7 @@ OPTION_FREE_VALID_ADDRESS= # Fail if NULL is used as input to free ...@@ -388,7 +388,7 @@ OPTION_FREE_VALID_ADDRESS= # Fail if NULL is used as input to free
OPTION_VALIDATE_FORMAT_STRINGS= # Runtime format string validation OPTION_VALIDATE_FORMAT_STRINGS= # Runtime format string validation
OPTION_LIBC_REPLACEMENTS= # Replace libc functions with RTL definitions OPTION_LIBC_REPLACEMENTS= # Replace libc functions with RTL definitions
OPTION_RTE_SELECT= # Generate assertions for these functions only OPTION_RTE_SELECT= # Generate assertions for these functions only
OPTION_THEN= # Adds -then in front of -e-acsl in FC command. OPTION_THEN= # Adds -then* in front of -e-acsl in FC command.
OPTION_STACK_SIZE= # Size of a heap shadow space (in MB) OPTION_STACK_SIZE= # Size of a heap shadow space (in MB)
OPTION_HEAP_SIZE= # Size of a stack shadow space (in MB) OPTION_HEAP_SIZE= # Size of a stack shadow space (in MB)
OPTIONS_TLS_SIZE= # Size of a TLS shadow space (in MB) OPTIONS_TLS_SIZE= # Size of a TLS shadow space (in MB)
...@@ -657,6 +657,11 @@ do ...@@ -657,6 +657,11 @@ do
shift; shift;
OPTION_THEN=-then OPTION_THEN=-then
;; ;;
# Separate extra Frama-C flags from e-acsl launch with -then-last.
--then-last)
shift;
OPTION_THEN=-then-last
;;
# Extra E-ACSL options # Extra E-ACSL options
--e-acsl-extra) --e-acsl-extra)
shift; shift;
......
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