Project

General

Profile

Download (2.5 KB) Statistics
| Branch: | Tag: | Revision:
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

    
(837-837/1153)