diff --git a/tests/libc/runtime.c b/tests/libc/runtime.c index 4ddb32fbb5c8dfcd6aae7415de4ba865ed028e49..25588a82e04f0833265e745ac70217161f1b0ef7 100644 --- a/tests/libc/runtime.c +++ b/tests/libc/runtime.c @@ -1,7 +1,7 @@ /* run.config* COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...) - CMD: @frama-c@ -print-machdep-header > __fc_machdep.h && gcc -I. -D__FC_MACHDEP_X86_64 @FRAMAC_SHARE@/libc/__fc_runtime.c -Wno-attributes -std=c99 -Wall -Wwrite-strings -o @DEV_NULL@ - OPT: + CMD: FRAMAC='@frama-c@' %{dep:@PTEST_DIR@/runtime.sh} + OPT: %{dep:@FRAMAC_SHARE@/libc/__fc_runtime.c} */ int main() { diff --git a/tests/libc/runtime.sh b/tests/libc/runtime.sh new file mode 100755 index 0000000000000000000000000000000000000000..aee0cf3d823f1aa61f34db70db8fd8caae2f4239 --- /dev/null +++ b/tests/libc/runtime.sh @@ -0,0 +1,7 @@ +#!/bin/sh +set -e +if test -z "$FRAMAC"; then echo "variable FRAMAC must be set"; exit 1; fi +TMPDIR=$(mktemp -d fc_test_libc_XXXXXXXX) +$FRAMAC -print-machdep-header > $TMPDIR/__fc_machdep.h +gcc -I$TMPDIR -D__FC_MACHDEP_X86_64 $@ -Wno-attributes -std=c99 -Wall -Wwrite-strings -o /dev/null +rm -fr $TMPDIR