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

[tests] fix tests broken when directory 'tests/bts' has been introduced

parent ea445466
No related branches found
No related tags found
No related merge requests found
Showing
with 49 additions and 40 deletions
#!/bin/sh
./gcc_test.sh bts $@
#!/bin/sh
./gcc_test.sh e-acsl-runtime $@
#!/bin/sh
IN=$1
if [ $# -gt 1 ]; then
shift;
DIR=$1
IN=$2
if [ $# -gt 2 ]; then
shift
shift
BUILTIN=$1
shift;
ARGS=$@
fi
gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/e-acsl-runtime/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$IN.c -lgmp && ./tests/e-acsl-runtime/result/gen_$IN.out $ARGS
gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/e-acsl-runtime/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_list.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$IN.c -lgmp && ./tests/e-acsl-runtime/result/gen_$IN.out $ARGS
gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_list.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/e-acsl-runtime/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_splay_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$IN.c -lgmp && ./tests/e-acsl-runtime/result/gen_$IN.out $ARGS
gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_splay_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/e-acsl-runtime/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$IN.c -lgmp && ./tests/e-acsl-runtime/result/gen_$IN.out $ARGS
gcc -std=c99 -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $BUILTIN -o ./tests/$DIR/result/gen_$IN.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/$DIR/result/gen_$IN.c -lgmp && ./tests/$DIR/result/gen_$IN.out $ARGS
/* run.config
COMMENT: argument of functions must be kept, so keep its parameter
EXECNOW: LOG gen_bts1304.c BIN gen_bts1304.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1304.c > /dev/null && ./gcc_test.sh bts1304
EXECNOW: LOG gen_bts13042.c BIN gen_bts13042.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13042.c > /dev/null && ./gcc_test.sh bts13042
EXECNOW: LOG gen_bts1304.c BIN gen_bts1304.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1304.c > /dev/null && ./gcc_bts.sh bts1304
EXECNOW: LOG gen_bts13042.c BIN gen_bts13042.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13042.c > /dev/null && ./gcc_bts.sh bts13042
*/
struct msgA { int type; int a[2]; };
......
/* run.config
COMMENT: spec with floats and reals
EXECNOW: LOG gen_bts1307.c BIN gen_bts1307.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1307.c > /dev/null && ./gcc_test.sh bts1307
EXECNOW: LOG gen_bts13072.c BIN gen_bts13072.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13072.c > /dev/null && ./gcc_test.sh bts13072
EXECNOW: LOG gen_bts1307.c BIN gen_bts1307.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1307.c > /dev/null && ./gcc_bts.sh bts1307
EXECNOW: LOG gen_bts13072.c BIN gen_bts13072.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13072.c > /dev/null && ./gcc_bts.sh bts13072
*/
/*@ requires \valid(Mtmax_in);
......
/* run.config
COMMENT: fixed bug with typing of universal quantification
EXECNOW: LOG gen_bts1324.c BIN gen_bts1324.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1324.c > /dev/null && ./gcc_test.sh bts1324
EXECNOW: LOG gen_bts13242.c BIN gen_bts13242.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13242.c > /dev/null && ./gcc_test.sh bts13242
EXECNOW: LOG gen_bts1324.c BIN gen_bts1324.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1324.c > /dev/null && ./gcc_bts.sh bts1324
EXECNOW: LOG gen_bts13242.c BIN gen_bts13242.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13242.c > /dev/null && ./gcc_bts.sh bts13242
*/
/*@ behavior yes:
......
/* run.config
COMMENT: complex term left-values
EXECNOW: LOG gen_bts1326.c BIN gen_bts1326.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1326.c > /dev/null && ./gcc_test.sh bts1326
EXECNOW: LOG gen_bts13262.c BIN gen_bts13262.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13262.c > /dev/null && ./gcc_test.sh bts13262
EXECNOW: LOG gen_bts1326.c BIN gen_bts1326.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1326.c > /dev/null && ./gcc_bts.sh bts1326
EXECNOW: LOG gen_bts13262.c BIN gen_bts13262.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13262.c > /dev/null && ./gcc_bts.sh bts13262
*/
typedef int ArrayInt[5];
......
/* run.config
COMMENT: bts #1390, issue with typing of quantified variables
STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
EXECNOW: LOG gen_bts1390.c BIN gen_bts1390.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1390.c > /dev/null && ./gcc_test.sh bts1390
EXECNOW: LOG gen_bts13902.c BIN gen_bts13902.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13902.c > /dev/null && ./gcc_test.sh bts13902
EXECNOW: LOG gen_bts1390.c BIN gen_bts1390.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1390.c > /dev/null && ./gcc_bts.sh bts1390
EXECNOW: LOG gen_bts13902.c BIN gen_bts13902.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13902.c > /dev/null && ./gcc_bts.sh bts13902
*/
#include "stdlib.h"
......
/* run.config
COMMENT: variadic function call
STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
EXECNOW: LOG gen_bts1398.c BIN gen_bts1398.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1398.c > /dev/null && ./gcc_test.sh bts1398 > /dev/null
EXECNOW: LOG gen_bts13982.c BIN gen_bts13982.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13982.c > /dev/null && ./gcc_test.sh bts13982 > /dev/null
EXECNOW: LOG gen_bts1398.c BIN gen_bts1398.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1398.c > /dev/null && ./gcc_bts.sh bts1398 > /dev/null
EXECNOW: LOG gen_bts13982.c BIN gen_bts13982.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13982.c > /dev/null && ./gcc_bts.sh bts13982 > /dev/null
*/
#include "stdio.h"
......
/* run.config
COMMENT: complex fields and indexes + potential RTE in \initialized
STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
EXECNOW: LOG gen_bts1399.c BIN gen_bts1399.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1399.c > /dev/null && ./gcc_test.sh bts1399
EXECNOW: LOG gen_bts13992.c BIN gen_bts13992.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13992.c > /dev/null && ./gcc_test.sh bts13992
EXECNOW: LOG gen_bts1399.c BIN gen_bts1399.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1399.c > /dev/null && ./gcc_bts.sh bts1399
EXECNOW: LOG gen_bts13992.c BIN gen_bts13992.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13992.c > /dev/null && ./gcc_bts.sh bts13992
*/
#include "stdlib.h"
......
/* run.config
COMMENT: bts #1478 about wrong detection of initializers in pre-analysis
EXECNOW: LOG gen_bts1478.c BIN gen_bts1478.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1478.c > /dev/null && ./gcc_test.sh bts1478
EXECNOW: LOG gen_bts14782.c BIN gen_bts14782.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts14782.c > /dev/null && ./gcc_test.sh bts14782
EXECNOW: LOG gen_bts1478.c BIN gen_bts1478.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1478.c > /dev/null && ./gcc_bts.sh bts1478
EXECNOW: LOG gen_bts14782.c BIN gen_bts14782.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts14782.c > /dev/null && ./gcc_bts.sh bts14782
*/
int global_i;
......
/* run.config
COMMENT: pointer to an empty struct
EXECNOW: LOG gen_bts1700.c BIN gen_bts1700.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1700.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1700.c > /dev/null && ./gcc_test.sh bts1700
EXECNOW: LOG gen_bts1700.c BIN gen_bts1700.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1700.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1700.c > /dev/null && ./gcc_bts.sh bts1700
*/
struct toto {};
......
/* run.config
COMMENT: bts #1717, issue with labels on memory-related statements
STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
EXECNOW: LOG gen_bts1717.c BIN gen_bts1717.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1717.c > /dev/null && ./gcc_test.sh bts1717
EXECNOW: LOG gen_bts17172.c BIN gen_bts17172.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts17172.c > /dev/null && ./gcc_test.sh bts17172
EXECNOW: LOG gen_bts1717.c BIN gen_bts1717.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1717.c > /dev/null && ./gcc_bts.sh bts1717
EXECNOW: LOG gen_bts17172.c BIN gen_bts17172.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts17172.c > /dev/null && ./gcc_bts.sh bts17172
*/
int main(void) {
......
/* run.config
COMMENT: addrOf
EXECNOW: LOG gen_addrOf.c BIN gen_addrOf.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/addrOf.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf.c > /dev/null && ./gcc_test.sh addrOf
EXECNOW: LOG gen_addrOf2.c BIN gen_addrOf2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/addrOf.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf2.c > /dev/null && ./gcc_test.sh addrOf2
EXECNOW: LOG gen_addrOf.c BIN gen_addrOf.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/addrOf.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf.c > /dev/null && ./gcc_runtime.sh addrOf
EXECNOW: LOG gen_addrOf2.c BIN gen_addrOf2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/addrOf.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf2.c > /dev/null && ./gcc_runtime.sh addrOf2
*/
void f(){
......
/* run.config
COMMENT: alias
EXECNOW: LOG gen_alias.c BIN gen_alias.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/alias.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_alias.c > /dev/null && ./gcc_test.sh alias
EXECNOW: LOG gen_alias2.c BIN gen_alias2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/alias.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_alias2.c > /dev/null && ./gcc_test.sh alias2
EXECNOW: LOG gen_alias.c BIN gen_alias.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/alias.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_alias.c > /dev/null && ./gcc_runtime.sh alias
EXECNOW: LOG gen_alias2.c BIN gen_alias2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/alias.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_alias2.c > /dev/null && ./gcc_runtime.sh alias2
*/
void f(int* dest, int val)
......
/* run.config
COMMENT: arithmetic operations
COMMENT: add the last assertion when fixing BTS #751
EXECNOW: LOG gen_arith.c BIN gen_arith.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/arith.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && ./gcc_test.sh arith
EXECNOW: LOG gen_arith2.c BIN gen_arith2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/arith.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_arith2.c > /dev/null && ./gcc_test.sh arith2
EXECNOW: LOG gen_arith.c BIN gen_arith.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/arith.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_arith.c > /dev/null && ./gcc_runtime.sh arith
EXECNOW: LOG gen_arith2.c BIN gen_arith2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/arith.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_arith2.c > /dev/null && ./gcc_runtime.sh arith2
*/
int main(void) {
......
/* run.config
COMMENT: arrays
STDOPT: #"-slevel 5"
EXECNOW: LOG gen_array.c BIN gen_array.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/array.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_array.c > /dev/null && ./gcc_test.sh array
EXECNOW: LOG gen_array2.c BIN gen_array2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/array.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_array2.c > /dev/null && ./gcc_test.sh array2
EXECNOW: LOG gen_array.c BIN gen_array.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/array.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_array.c > /dev/null && ./gcc_runtime.sh array
EXECNOW: LOG gen_array2.c BIN gen_array2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/array.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_array2.c > /dev/null && ./gcc_runtime.sh array2
*/
int T1[3],T2[4];
......
/* run.config
COMMENT: \at
EXECNOW: LOG gen_at.c BIN gen_at.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/at.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && ./gcc_test.sh at -Wno-unused-label
EXECNOW: LOG gen_at2.c BIN gen_at2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/at.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_at2.c > /dev/null && ./gcc_test.sh at2 -Wno-unused-label
EXECNOW: LOG gen_at.c BIN gen_at.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/at.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && ./gcc_runtime.sh at -Wno-unused-label
EXECNOW: LOG gen_at2.c BIN gen_at2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/at.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_at2.c > /dev/null && ./gcc_runtime.sh at2 -Wno-unused-label
*/
int A = 0;
......
/* run.config
COMMENT: function call
STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
EXECNOW: LOG gen_call.c BIN gen_call.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/call.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_call.c > /dev/null && ./gcc_test.sh call
EXECNOW: LOG gen_call2.c BIN gen_call2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/call.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_call2.c > /dev/null && ./gcc_test.sh call2
EXECNOW: LOG gen_call.c BIN gen_call.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/call.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_call.c > /dev/null && ./gcc_runtime.sh call
EXECNOW: LOG gen_call2.c BIN gen_call2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/call.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_call2.c > /dev/null && ./gcc_runtime.sh call2
*/
#include <stdlib.h>
......
/* run.config
COMMENT: cast
STDOPT: #"-no-warn-signed-downcast" #"-no-warn-unsigned-downcast"
EXECNOW: LOG gen_cast.c BIN gen_cast.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/cast.i -e-acsl -no-warn-signed-downcast -no-warn-unsigned-downcast -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && ./gcc_test.sh cast
EXECNOW: LOG gen_cast2.c BIN gen_cast2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/cast.i -e-acsl-gmp-only -no-warn-signed-downcast -no-warn-unsigned-downcast -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_cast2.c > /dev/null && ./gcc_test.sh cast2
EXECNOW: LOG gen_cast.c BIN gen_cast.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/cast.i -e-acsl -no-warn-signed-downcast -no-warn-unsigned-downcast -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_cast.c > /dev/null && ./gcc_runtime.sh cast
EXECNOW: LOG gen_cast2.c BIN gen_cast2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/cast.i -e-acsl-gmp-only -no-warn-signed-downcast -no-warn-unsigned-downcast -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_cast2.c > /dev/null && ./gcc_runtime.sh cast2
*/
int main(void) {
......
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