Revision cd1faebc
Added by Pierre-Loïc Garoche about 4 years ago
| regression_tests/lustre_files/success/Simulink/src_many_files/Assignment2_PP.LUSTREC.makefile | ||
|---|---|---|
| 1 |
BINNAME?=Assignment2_PP.LUSTREC_Assignment2_PP |
|
| 2 |
GCC=gcc -O0 |
|
| 3 |
LUSTREC=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/bin/lustrec |
|
| 4 |
LUSTREC_BASE=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx |
|
| 5 |
INC=${LUSTREC_BASE}/include/lustrec
|
|
| 6 |
|
|
| 7 |
Assignment2_PP.LUSTREC_run: Assignment2_PP.LUSTREC.c Assignment2_PP.LUSTREC_main.c |
|
| 8 |
${GCC} -I${INC} -I. -c Assignment2_PP.LUSTREC.c
|
|
| 9 |
${GCC} -I${INC} -I. -c Assignment2_PP.LUSTREC_main.c
|
|
| 10 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 11 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 12 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 13 |
${GCC} -o ${BINNAME} io_frontend.o conv.o mpfr_lustre.o Assignment2_PP.LUSTREC.o Assignment2_PP.LUSTREC_main.o -lmpfr -lgmp
|
|
| 14 |
|
|
| 15 |
clean: |
|
| 16 |
\rm -f *.o ${BINNAME}
|
|
| 17 |
|
|
| 18 |
FRAMACEACSL=`frama-c -print-share-path`/e-acsl |
|
| 19 |
Assignment2_PP.LUSTREC_eacsl.c: Assignment2_PP.LUSTREC.c Assignment2_PP.LUSTREC.h |
|
| 20 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Assignment2_PP.LUSTREC.c -then-on e-acsl -print -ocode Assignment2_PP.LUSTREC_eacsl.c |
|
| 21 |
|
|
| 22 |
|
|
| 23 |
Assignment2_PP.LUSTREC_main_eacsl.c: Assignment2_PP.LUSTREC.c Assignment2_PP.LUSTREC.h Assignment2_PP.LUSTREC_main.c |
|
| 24 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Assignment2_PP.LUSTREC.c Assignment2_PP.LUSTREC_main.c -then-on e-acsl -print -ocode Assignment2_PP.LUSTREC_main_eacsl.i |
|
| 25 |
grep -v _fc_stdout Assignment2_PP.LUSTREC_main_eacsl.i > Assignment2_PP.LUSTREC_main_eacsl.c |
|
| 26 |
|
|
| 27 |
Assignment2_PP.LUSTREC_main_eacsl: Assignment2_PP.LUSTREC_main_eacsl.c |
|
| 28 |
${GCC} -Wno-attributes -I${INC} -I. -c Assignment2_PP.LUSTREC_main_eacsl.c
|
|
| 29 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 30 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 31 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 32 |
${GCC} -Wno-attributes -o Assignment2_PP.LUSTREC_main_eacsl io_frontend.o conv.o mpfr_lustre.o ${FRAMACEACSL}/e_acsl.c ${FRAMACEACSL}/memory_model/e_acsl_bittree.c ${FRAMACEACSL}/memory_model/e_acsl_mmodel.c Assignment2_PP.LUSTREC_main_eacsl.o -lmpfr -lgmp
|
|
| 33 |
|
|
| 34 |
|
|
| regression_tests/lustre_files/success/Simulink/src_many_files/Assignment6_PP.LUSTREC.makefile | ||
|---|---|---|
| 1 |
BINNAME?=Assignment6_PP.LUSTREC_Assignment6_PP |
|
| 2 |
GCC=gcc -O0 |
|
| 3 |
LUSTREC=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/bin/lustrec |
|
| 4 |
LUSTREC_BASE=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx |
|
| 5 |
INC=${LUSTREC_BASE}/include/lustrec
|
|
| 6 |
|
|
| 7 |
Assignment6_PP.LUSTREC_run: Assignment6_PP.LUSTREC.c Assignment6_PP.LUSTREC_main.c |
|
| 8 |
${GCC} -I${INC} -I. -c Assignment6_PP.LUSTREC.c
|
|
| 9 |
${GCC} -I${INC} -I. -c Assignment6_PP.LUSTREC_main.c
|
|
| 10 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 11 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 12 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 13 |
${GCC} -o ${BINNAME} io_frontend.o conv.o mpfr_lustre.o Assignment6_PP.LUSTREC.o Assignment6_PP.LUSTREC_main.o -lmpfr -lgmp
|
|
| 14 |
|
|
| 15 |
clean: |
|
| 16 |
\rm -f *.o ${BINNAME}
|
|
| 17 |
|
|
| 18 |
FRAMACEACSL=`frama-c -print-share-path`/e-acsl |
|
| 19 |
Assignment6_PP.LUSTREC_eacsl.c: Assignment6_PP.LUSTREC.c Assignment6_PP.LUSTREC.h |
|
| 20 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Assignment6_PP.LUSTREC.c -then-on e-acsl -print -ocode Assignment6_PP.LUSTREC_eacsl.c |
|
| 21 |
|
|
| 22 |
|
|
| 23 |
Assignment6_PP.LUSTREC_main_eacsl.c: Assignment6_PP.LUSTREC.c Assignment6_PP.LUSTREC.h Assignment6_PP.LUSTREC_main.c |
|
| 24 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Assignment6_PP.LUSTREC.c Assignment6_PP.LUSTREC_main.c -then-on e-acsl -print -ocode Assignment6_PP.LUSTREC_main_eacsl.i |
|
| 25 |
grep -v _fc_stdout Assignment6_PP.LUSTREC_main_eacsl.i > Assignment6_PP.LUSTREC_main_eacsl.c |
|
| 26 |
|
|
| 27 |
Assignment6_PP.LUSTREC_main_eacsl: Assignment6_PP.LUSTREC_main_eacsl.c |
|
| 28 |
${GCC} -Wno-attributes -I${INC} -I. -c Assignment6_PP.LUSTREC_main_eacsl.c
|
|
| 29 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 30 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 31 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 32 |
${GCC} -Wno-attributes -o Assignment6_PP.LUSTREC_main_eacsl io_frontend.o conv.o mpfr_lustre.o ${FRAMACEACSL}/e_acsl.c ${FRAMACEACSL}/memory_model/e_acsl_bittree.c ${FRAMACEACSL}/memory_model/e_acsl_mmodel.c Assignment6_PP.LUSTREC_main_eacsl.o -lmpfr -lgmp
|
|
| 33 |
|
|
| 34 |
|
|
| regression_tests/lustre_files/success/Simulink/src_many_files/Assignment7_PP.LUSTREC.makefile | ||
|---|---|---|
| 1 |
BINNAME?=Assignment7_PP.LUSTREC_Assignment7_PP |
|
| 2 |
GCC=gcc -O0 |
|
| 3 |
LUSTREC=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/bin/lustrec |
|
| 4 |
LUSTREC_BASE=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx |
|
| 5 |
INC=${LUSTREC_BASE}/include/lustrec
|
|
| 6 |
|
|
| 7 |
Assignment7_PP.LUSTREC_run: Assignment7_PP.LUSTREC.c Assignment7_PP.LUSTREC_main.c |
|
| 8 |
${GCC} -I${INC} -I. -c Assignment7_PP.LUSTREC.c
|
|
| 9 |
${GCC} -I${INC} -I. -c Assignment7_PP.LUSTREC_main.c
|
|
| 10 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 11 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 12 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 13 |
${GCC} -o ${BINNAME} io_frontend.o conv.o mpfr_lustre.o Assignment7_PP.LUSTREC.o Assignment7_PP.LUSTREC_main.o -lmpfr -lgmp
|
|
| 14 |
|
|
| 15 |
clean: |
|
| 16 |
\rm -f *.o ${BINNAME}
|
|
| 17 |
|
|
| 18 |
FRAMACEACSL=`frama-c -print-share-path`/e-acsl |
|
| 19 |
Assignment7_PP.LUSTREC_eacsl.c: Assignment7_PP.LUSTREC.c Assignment7_PP.LUSTREC.h |
|
| 20 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Assignment7_PP.LUSTREC.c -then-on e-acsl -print -ocode Assignment7_PP.LUSTREC_eacsl.c |
|
| 21 |
|
|
| 22 |
|
|
| 23 |
Assignment7_PP.LUSTREC_main_eacsl.c: Assignment7_PP.LUSTREC.c Assignment7_PP.LUSTREC.h Assignment7_PP.LUSTREC_main.c |
|
| 24 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Assignment7_PP.LUSTREC.c Assignment7_PP.LUSTREC_main.c -then-on e-acsl -print -ocode Assignment7_PP.LUSTREC_main_eacsl.i |
|
| 25 |
grep -v _fc_stdout Assignment7_PP.LUSTREC_main_eacsl.i > Assignment7_PP.LUSTREC_main_eacsl.c |
|
| 26 |
|
|
| 27 |
Assignment7_PP.LUSTREC_main_eacsl: Assignment7_PP.LUSTREC_main_eacsl.c |
|
| 28 |
${GCC} -Wno-attributes -I${INC} -I. -c Assignment7_PP.LUSTREC_main_eacsl.c
|
|
| 29 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 30 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 31 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 32 |
${GCC} -Wno-attributes -o Assignment7_PP.LUSTREC_main_eacsl io_frontend.o conv.o mpfr_lustre.o ${FRAMACEACSL}/e_acsl.c ${FRAMACEACSL}/memory_model/e_acsl_bittree.c ${FRAMACEACSL}/memory_model/e_acsl_mmodel.c Assignment7_PP.LUSTREC_main_eacsl.o -lmpfr -lgmp
|
|
| 33 |
|
|
| 34 |
|
|
| regression_tests/lustre_files/success/Simulink/src_many_files/Assignment8_PP.LUSTREC.makefile | ||
|---|---|---|
| 1 |
BINNAME?=Assignment8_PP.LUSTREC_Assignment8_PP |
|
| 2 |
GCC=gcc -O0 |
|
| 3 |
LUSTREC=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/bin/lustrec |
|
| 4 |
LUSTREC_BASE=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx |
|
| 5 |
INC=${LUSTREC_BASE}/include/lustrec
|
|
| 6 |
|
|
| 7 |
Assignment8_PP.LUSTREC_run: Assignment8_PP.LUSTREC.c Assignment8_PP.LUSTREC_main.c |
|
| 8 |
${GCC} -I${INC} -I. -c Assignment8_PP.LUSTREC.c
|
|
| 9 |
${GCC} -I${INC} -I. -c Assignment8_PP.LUSTREC_main.c
|
|
| 10 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 11 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 12 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 13 |
${GCC} -o ${BINNAME} io_frontend.o conv.o mpfr_lustre.o Assignment8_PP.LUSTREC.o Assignment8_PP.LUSTREC_main.o -lmpfr -lgmp
|
|
| 14 |
|
|
| 15 |
clean: |
|
| 16 |
\rm -f *.o ${BINNAME}
|
|
| 17 |
|
|
| 18 |
FRAMACEACSL=`frama-c -print-share-path`/e-acsl |
|
| 19 |
Assignment8_PP.LUSTREC_eacsl.c: Assignment8_PP.LUSTREC.c Assignment8_PP.LUSTREC.h |
|
| 20 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Assignment8_PP.LUSTREC.c -then-on e-acsl -print -ocode Assignment8_PP.LUSTREC_eacsl.c |
|
| 21 |
|
|
| 22 |
|
|
| 23 |
Assignment8_PP.LUSTREC_main_eacsl.c: Assignment8_PP.LUSTREC.c Assignment8_PP.LUSTREC.h Assignment8_PP.LUSTREC_main.c |
|
| 24 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Assignment8_PP.LUSTREC.c Assignment8_PP.LUSTREC_main.c -then-on e-acsl -print -ocode Assignment8_PP.LUSTREC_main_eacsl.i |
|
| 25 |
grep -v _fc_stdout Assignment8_PP.LUSTREC_main_eacsl.i > Assignment8_PP.LUSTREC_main_eacsl.c |
|
| 26 |
|
|
| 27 |
Assignment8_PP.LUSTREC_main_eacsl: Assignment8_PP.LUSTREC_main_eacsl.c |
|
| 28 |
${GCC} -Wno-attributes -I${INC} -I. -c Assignment8_PP.LUSTREC_main_eacsl.c
|
|
| 29 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 30 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 31 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 32 |
${GCC} -Wno-attributes -o Assignment8_PP.LUSTREC_main_eacsl io_frontend.o conv.o mpfr_lustre.o ${FRAMACEACSL}/e_acsl.c ${FRAMACEACSL}/memory_model/e_acsl_bittree.c ${FRAMACEACSL}/memory_model/e_acsl_mmodel.c Assignment8_PP.LUSTREC_main_eacsl.o -lmpfr -lgmp
|
|
| 33 |
|
|
| 34 |
|
|
| regression_tests/lustre_files/success/Simulink/src_many_files/Assignment9_PP.LUSTREC.makefile | ||
|---|---|---|
| 1 |
BINNAME?=Assignment9_PP.LUSTREC_Assignment9_PP |
|
| 2 |
GCC=gcc -O0 |
|
| 3 |
LUSTREC=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/bin/lustrec |
|
| 4 |
LUSTREC_BASE=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx |
|
| 5 |
INC=${LUSTREC_BASE}/include/lustrec
|
|
| 6 |
|
|
| 7 |
Assignment9_PP.LUSTREC_run: Assignment9_PP.LUSTREC.c Assignment9_PP.LUSTREC_main.c |
|
| 8 |
${GCC} -I${INC} -I. -c Assignment9_PP.LUSTREC.c
|
|
| 9 |
${GCC} -I${INC} -I. -c Assignment9_PP.LUSTREC_main.c
|
|
| 10 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 11 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 12 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 13 |
${GCC} -o ${BINNAME} io_frontend.o conv.o mpfr_lustre.o Assignment9_PP.LUSTREC.o Assignment9_PP.LUSTREC_main.o -lmpfr -lgmp
|
|
| 14 |
|
|
| 15 |
clean: |
|
| 16 |
\rm -f *.o ${BINNAME}
|
|
| 17 |
|
|
| 18 |
FRAMACEACSL=`frama-c -print-share-path`/e-acsl |
|
| 19 |
Assignment9_PP.LUSTREC_eacsl.c: Assignment9_PP.LUSTREC.c Assignment9_PP.LUSTREC.h |
|
| 20 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Assignment9_PP.LUSTREC.c -then-on e-acsl -print -ocode Assignment9_PP.LUSTREC_eacsl.c |
|
| 21 |
|
|
| 22 |
|
|
| 23 |
Assignment9_PP.LUSTREC_main_eacsl.c: Assignment9_PP.LUSTREC.c Assignment9_PP.LUSTREC.h Assignment9_PP.LUSTREC_main.c |
|
| 24 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Assignment9_PP.LUSTREC.c Assignment9_PP.LUSTREC_main.c -then-on e-acsl -print -ocode Assignment9_PP.LUSTREC_main_eacsl.i |
|
| 25 |
grep -v _fc_stdout Assignment9_PP.LUSTREC_main_eacsl.i > Assignment9_PP.LUSTREC_main_eacsl.c |
|
| 26 |
|
|
| 27 |
Assignment9_PP.LUSTREC_main_eacsl: Assignment9_PP.LUSTREC_main_eacsl.c |
|
| 28 |
${GCC} -Wno-attributes -I${INC} -I. -c Assignment9_PP.LUSTREC_main_eacsl.c
|
|
| 29 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 30 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 31 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 32 |
${GCC} -Wno-attributes -o Assignment9_PP.LUSTREC_main_eacsl io_frontend.o conv.o mpfr_lustre.o ${FRAMACEACSL}/e_acsl.c ${FRAMACEACSL}/memory_model/e_acsl_bittree.c ${FRAMACEACSL}/memory_model/e_acsl_mmodel.c Assignment9_PP.LUSTREC_main_eacsl.o -lmpfr -lgmp
|
|
| 33 |
|
|
| 34 |
|
|
| regression_tests/lustre_files/success/Simulink/src_many_files/Assignment_PP.LUSTREC.makefile | ||
|---|---|---|
| 1 |
BINNAME?=Assignment_PP.LUSTREC_Assignment_PP |
|
| 2 |
GCC=gcc -O0 |
|
| 3 |
LUSTREC=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/bin/lustrec |
|
| 4 |
LUSTREC_BASE=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx |
|
| 5 |
INC=${LUSTREC_BASE}/include/lustrec
|
|
| 6 |
|
|
| 7 |
Assignment_PP.LUSTREC_run: Assignment_PP.LUSTREC.c Assignment_PP.LUSTREC_main.c |
|
| 8 |
${GCC} -I${INC} -I. -c Assignment_PP.LUSTREC.c
|
|
| 9 |
${GCC} -I${INC} -I. -c Assignment_PP.LUSTREC_main.c
|
|
| 10 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 11 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 12 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 13 |
${GCC} -o ${BINNAME} io_frontend.o conv.o mpfr_lustre.o Assignment_PP.LUSTREC.o Assignment_PP.LUSTREC_main.o -lmpfr -lgmp
|
|
| 14 |
|
|
| 15 |
clean: |
|
| 16 |
\rm -f *.o ${BINNAME}
|
|
| 17 |
|
|
| 18 |
FRAMACEACSL=`frama-c -print-share-path`/e-acsl |
|
| 19 |
Assignment_PP.LUSTREC_eacsl.c: Assignment_PP.LUSTREC.c Assignment_PP.LUSTREC.h |
|
| 20 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Assignment_PP.LUSTREC.c -then-on e-acsl -print -ocode Assignment_PP.LUSTREC_eacsl.c |
|
| 21 |
|
|
| 22 |
|
|
| 23 |
Assignment_PP.LUSTREC_main_eacsl.c: Assignment_PP.LUSTREC.c Assignment_PP.LUSTREC.h Assignment_PP.LUSTREC_main.c |
|
| 24 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Assignment_PP.LUSTREC.c Assignment_PP.LUSTREC_main.c -then-on e-acsl -print -ocode Assignment_PP.LUSTREC_main_eacsl.i |
|
| 25 |
grep -v _fc_stdout Assignment_PP.LUSTREC_main_eacsl.i > Assignment_PP.LUSTREC_main_eacsl.c |
|
| 26 |
|
|
| 27 |
Assignment_PP.LUSTREC_main_eacsl: Assignment_PP.LUSTREC_main_eacsl.c |
|
| 28 |
${GCC} -Wno-attributes -I${INC} -I. -c Assignment_PP.LUSTREC_main_eacsl.c
|
|
| 29 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 30 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 31 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 32 |
${GCC} -Wno-attributes -o Assignment_PP.LUSTREC_main_eacsl io_frontend.o conv.o mpfr_lustre.o ${FRAMACEACSL}/e_acsl.c ${FRAMACEACSL}/memory_model/e_acsl_bittree.c ${FRAMACEACSL}/memory_model/e_acsl_mmodel.c Assignment_PP.LUSTREC_main_eacsl.o -lmpfr -lgmp
|
|
| 33 |
|
|
| 34 |
|
|
| regression_tests/lustre_files/success/Simulink/src_many_files/Assignment_port_3.LUSTREC.makefile | ||
|---|---|---|
| 1 |
BINNAME?=Assignment_port_3.LUSTREC_Assignment_port_3 |
|
| 2 |
GCC=gcc -O0 |
|
| 3 |
LUSTREC=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/bin/lustrec |
|
| 4 |
LUSTREC_BASE=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx |
|
| 5 |
INC=${LUSTREC_BASE}/include/lustrec
|
|
| 6 |
|
|
| 7 |
Assignment_port_3.LUSTREC_run: Assignment_port_3.LUSTREC.c Assignment_port_3.LUSTREC_main.c |
|
| 8 |
${GCC} -I${INC} -I. -c Assignment_port_3.LUSTREC.c
|
|
| 9 |
${GCC} -I${INC} -I. -c Assignment_port_3.LUSTREC_main.c
|
|
| 10 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 11 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 12 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 13 |
${GCC} -o ${BINNAME} io_frontend.o conv.o mpfr_lustre.o Assignment_port_3.LUSTREC.o Assignment_port_3.LUSTREC_main.o -lmpfr -lgmp
|
|
| 14 |
|
|
| 15 |
clean: |
|
| 16 |
\rm -f *.o ${BINNAME}
|
|
| 17 |
|
|
| 18 |
FRAMACEACSL=`frama-c -print-share-path`/e-acsl |
|
| 19 |
Assignment_port_3.LUSTREC_eacsl.c: Assignment_port_3.LUSTREC.c Assignment_port_3.LUSTREC.h |
|
| 20 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Assignment_port_3.LUSTREC.c -then-on e-acsl -print -ocode Assignment_port_3.LUSTREC_eacsl.c |
|
| 21 |
|
|
| 22 |
|
|
| 23 |
Assignment_port_3.LUSTREC_main_eacsl.c: Assignment_port_3.LUSTREC.c Assignment_port_3.LUSTREC.h Assignment_port_3.LUSTREC_main.c |
|
| 24 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Assignment_port_3.LUSTREC.c Assignment_port_3.LUSTREC_main.c -then-on e-acsl -print -ocode Assignment_port_3.LUSTREC_main_eacsl.i |
|
| 25 |
grep -v _fc_stdout Assignment_port_3.LUSTREC_main_eacsl.i > Assignment_port_3.LUSTREC_main_eacsl.c |
|
| 26 |
|
|
| 27 |
Assignment_port_3.LUSTREC_main_eacsl: Assignment_port_3.LUSTREC_main_eacsl.c |
|
| 28 |
${GCC} -Wno-attributes -I${INC} -I. -c Assignment_port_3.LUSTREC_main_eacsl.c
|
|
| 29 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 30 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 31 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 32 |
${GCC} -Wno-attributes -o Assignment_port_3.LUSTREC_main_eacsl io_frontend.o conv.o mpfr_lustre.o ${FRAMACEACSL}/e_acsl.c ${FRAMACEACSL}/memory_model/e_acsl_bittree.c ${FRAMACEACSL}/memory_model/e_acsl_mmodel.c Assignment_port_3.LUSTREC_main_eacsl.o -lmpfr -lgmp
|
|
| 33 |
|
|
| 34 |
|
|
| regression_tests/lustre_files/success/Simulink/src_many_files/Bias_PP.LUSTREC.makefile | ||
|---|---|---|
| 1 |
BINNAME?=Bias_PP.LUSTREC_Bias_PP |
|
| 2 |
GCC=gcc -O0 |
|
| 3 |
LUSTREC=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/bin/lustrec |
|
| 4 |
LUSTREC_BASE=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx |
|
| 5 |
INC=${LUSTREC_BASE}/include/lustrec
|
|
| 6 |
|
|
| 7 |
Bias_PP.LUSTREC_run: Bias_PP.LUSTREC.c Bias_PP.LUSTREC_main.c |
|
| 8 |
${GCC} -I${INC} -I. -c Bias_PP.LUSTREC.c
|
|
| 9 |
${GCC} -I${INC} -I. -c Bias_PP.LUSTREC_main.c
|
|
| 10 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 11 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 12 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 13 |
${GCC} -o ${BINNAME} io_frontend.o conv.o mpfr_lustre.o Bias_PP.LUSTREC.o Bias_PP.LUSTREC_main.o -lmpfr -lgmp
|
|
| 14 |
|
|
| 15 |
clean: |
|
| 16 |
\rm -f *.o ${BINNAME}
|
|
| 17 |
|
|
| 18 |
FRAMACEACSL=`frama-c -print-share-path`/e-acsl |
|
| 19 |
Bias_PP.LUSTREC_eacsl.c: Bias_PP.LUSTREC.c Bias_PP.LUSTREC.h |
|
| 20 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Bias_PP.LUSTREC.c -then-on e-acsl -print -ocode Bias_PP.LUSTREC_eacsl.c |
|
| 21 |
|
|
| 22 |
|
|
| 23 |
Bias_PP.LUSTREC_main_eacsl.c: Bias_PP.LUSTREC.c Bias_PP.LUSTREC.h Bias_PP.LUSTREC_main.c |
|
| 24 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl Bias_PP.LUSTREC.c Bias_PP.LUSTREC_main.c -then-on e-acsl -print -ocode Bias_PP.LUSTREC_main_eacsl.i |
|
| 25 |
grep -v _fc_stdout Bias_PP.LUSTREC_main_eacsl.i > Bias_PP.LUSTREC_main_eacsl.c |
|
| 26 |
|
|
| 27 |
Bias_PP.LUSTREC_main_eacsl: Bias_PP.LUSTREC_main_eacsl.c |
|
| 28 |
${GCC} -Wno-attributes -I${INC} -I. -c Bias_PP.LUSTREC_main_eacsl.c
|
|
| 29 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 30 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 31 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 32 |
${GCC} -Wno-attributes -o Bias_PP.LUSTREC_main_eacsl io_frontend.o conv.o mpfr_lustre.o ${FRAMACEACSL}/e_acsl.c ${FRAMACEACSL}/memory_model/e_acsl_bittree.c ${FRAMACEACSL}/memory_model/e_acsl_mmodel.c Bias_PP.LUSTREC_main_eacsl.o -lmpfr -lgmp
|
|
| 33 |
|
|
| 34 |
|
|
| regression_tests/lustre_files/success/Simulink/src_many_files/DotProduct_PP.LUSTREC.makefile | ||
|---|---|---|
| 1 |
BINNAME?=DotProduct_PP.LUSTREC_DotProduct_PP |
|
| 2 |
GCC=gcc -O0 |
|
| 3 |
LUSTREC=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/bin/lustrec |
|
| 4 |
LUSTREC_BASE=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx |
|
| 5 |
INC=${LUSTREC_BASE}/include/lustrec
|
|
| 6 |
|
|
| 7 |
DotProduct_PP.LUSTREC_run: DotProduct_PP.LUSTREC.c DotProduct_PP.LUSTREC_main.c |
|
| 8 |
${GCC} -I${INC} -I. -c DotProduct_PP.LUSTREC.c
|
|
| 9 |
${GCC} -I${INC} -I. -c DotProduct_PP.LUSTREC_main.c
|
|
| 10 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 11 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 12 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 13 |
${GCC} -o ${BINNAME} io_frontend.o conv.o mpfr_lustre.o DotProduct_PP.LUSTREC.o DotProduct_PP.LUSTREC_main.o -lmpfr -lgmp
|
|
| 14 |
|
|
| 15 |
clean: |
|
| 16 |
\rm -f *.o ${BINNAME}
|
|
| 17 |
|
|
| 18 |
FRAMACEACSL=`frama-c -print-share-path`/e-acsl |
|
| 19 |
DotProduct_PP.LUSTREC_eacsl.c: DotProduct_PP.LUSTREC.c DotProduct_PP.LUSTREC.h |
|
| 20 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl DotProduct_PP.LUSTREC.c -then-on e-acsl -print -ocode DotProduct_PP.LUSTREC_eacsl.c |
|
| 21 |
|
|
| 22 |
|
|
| 23 |
DotProduct_PP.LUSTREC_main_eacsl.c: DotProduct_PP.LUSTREC.c DotProduct_PP.LUSTREC.h DotProduct_PP.LUSTREC_main.c |
|
| 24 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl DotProduct_PP.LUSTREC.c DotProduct_PP.LUSTREC_main.c -then-on e-acsl -print -ocode DotProduct_PP.LUSTREC_main_eacsl.i |
|
| 25 |
grep -v _fc_stdout DotProduct_PP.LUSTREC_main_eacsl.i > DotProduct_PP.LUSTREC_main_eacsl.c |
|
| 26 |
|
|
| 27 |
DotProduct_PP.LUSTREC_main_eacsl: DotProduct_PP.LUSTREC_main_eacsl.c |
|
| 28 |
${GCC} -Wno-attributes -I${INC} -I. -c DotProduct_PP.LUSTREC_main_eacsl.c
|
|
| 29 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 30 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 31 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 32 |
${GCC} -Wno-attributes -o DotProduct_PP.LUSTREC_main_eacsl io_frontend.o conv.o mpfr_lustre.o ${FRAMACEACSL}/e_acsl.c ${FRAMACEACSL}/memory_model/e_acsl_bittree.c ${FRAMACEACSL}/memory_model/e_acsl_mmodel.c DotProduct_PP.LUSTREC_main_eacsl.o -lmpfr -lgmp
|
|
| 33 |
|
|
| 34 |
|
|
| regression_tests/lustre_files/success/Simulink/src_many_files/LookupTable1D_output_int_PP.LUSTREC.makefile | ||
|---|---|---|
| 1 |
BINNAME?=LookupTable1D_output_int_PP.LUSTREC_LookupTable1D_output_int_PP |
|
| 2 |
GCC=gcc -O0 |
|
| 3 |
LUSTREC=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/bin/lustrec |
|
| 4 |
LUSTREC_BASE=/Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx |
|
| 5 |
INC=${LUSTREC_BASE}/include/lustrec
|
|
| 6 |
|
|
| 7 |
LookupTable1D_output_int_PP.LUSTREC_run: LookupTable1D_output_int_PP.LUSTREC.c LookupTable1D_output_int_PP.LUSTREC_main.c |
|
| 8 |
${GCC} -I${INC} -I. -c LookupTable1D_output_int_PP.LUSTREC.c
|
|
| 9 |
${GCC} -I${INC} -I. -c LookupTable1D_output_int_PP.LUSTREC_main.c
|
|
| 10 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 11 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 12 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 13 |
${GCC} -o ${BINNAME} io_frontend.o conv.o mpfr_lustre.o LookupTable1D_output_int_PP.LUSTREC.o LookupTable1D_output_int_PP.LUSTREC_main.o -lmpfr -lgmp
|
|
| 14 |
|
|
| 15 |
clean: |
|
| 16 |
\rm -f *.o ${BINNAME}
|
|
| 17 |
|
|
| 18 |
FRAMACEACSL=`frama-c -print-share-path`/e-acsl |
|
| 19 |
LookupTable1D_output_int_PP.LUSTREC_eacsl.c: LookupTable1D_output_int_PP.LUSTREC.c LookupTable1D_output_int_PP.LUSTREC.h |
|
| 20 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl LookupTable1D_output_int_PP.LUSTREC.c -then-on e-acsl -print -ocode LookupTable1D_output_int_PP.LUSTREC_eacsl.c |
|
| 21 |
|
|
| 22 |
|
|
| 23 |
LookupTable1D_output_int_PP.LUSTREC_main_eacsl.c: LookupTable1D_output_int_PP.LUSTREC.c LookupTable1D_output_int_PP.LUSTREC.h LookupTable1D_output_int_PP.LUSTREC_main.c |
|
| 24 |
frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl LookupTable1D_output_int_PP.LUSTREC.c LookupTable1D_output_int_PP.LUSTREC_main.c -then-on e-acsl -print -ocode LookupTable1D_output_int_PP.LUSTREC_main_eacsl.i |
|
| 25 |
grep -v _fc_stdout LookupTable1D_output_int_PP.LUSTREC_main_eacsl.i > LookupTable1D_output_int_PP.LUSTREC_main_eacsl.c |
|
| 26 |
|
|
| 27 |
LookupTable1D_output_int_PP.LUSTREC_main_eacsl: LookupTable1D_output_int_PP.LUSTREC_main_eacsl.c |
|
| 28 |
${GCC} -Wno-attributes -I${INC} -I. -c LookupTable1D_output_int_PP.LUSTREC_main_eacsl.c
|
|
| 29 |
${GCC} -I${INC} -c ${INC}/io_frontend.c
|
|
| 30 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/conv.c
|
|
| 31 |
${GCC} -I${INC} -c /Users/hbourbou/Documents/babelfish/cocosim2/tools/verifiers/osx/include/lustrec/mpfr_lustre.c
|
|
| 32 |
${GCC} -Wno-attributes -o LookupTable1D_output_int_PP.LUSTREC_main_eacsl io_frontend.o conv.o mpfr_lustre.o ${FRAMACEACSL}/e_acsl.c ${FRAMACEACSL}/memory_model/e_acsl_bittree.c ${FRAMACEACSL}/memory_model/e_acsl_mmodel.c LookupTable1D_output_int_PP.LUSTREC_main_eacsl.o -lmpfr -lgmp
|
|
| 33 |
|
|
| 34 |
|
|
Also available in: Unified diff
No temporary file on repo!