Project

General

Profile

Revision cd1faebc

View differences:

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