Project

General

Profile

Download (1.38 KB) Statistics
| Branch: | Tag: | Revision:
1
GCC=gcc
2
LUSTREC=/home/ploc/Local/bin/lustrec
3
LUSTREC_BASE=/home/ploc/Local
4
INC=${LUSTREC_BASE}/include/lustrec
5

    
6
example1_ControlSys_SFunction: example1.c example1_main.c
7
	${GCC} -O0 -I${INC} -I. -c example1.c
8
	${GCC} -O0 -I${INC} -I. -c example1_main.c
9
	${GCC} -I${INC} -c ${INC}/io_frontend.c
10
	${GCC} -I${INC} -c mydouble.c mydouble_wrapper.c
11
	${GCC} -O0 -o example1_ControlSys_SFunction io_frontend.o mydouble.o mydouble_wrapper.o example1.o example1_main.o 
12

    
13
clean:
14
	\rm -f *.o example1_ControlSys_SFunction
15

    
16
.PHONY: example1_ControlSys_SFunction
17

    
18
FRAMACEACSL=`frama-c -print-share-path`/e-acsl
19
example1_eacsl.c: example1.c example1.h
20
	frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl example1.c -then-on e-acsl -print -ocode example1_eacsl.c
21

    
22

    
23
example1_main_eacsl.c: example1.c example1.h example1_main.c
24
	frama-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl example1.c example1_main.c -then-on e-acsl -print -ocode example1_main_eacsl.i
25
	grep -v _fc_stdout example1_main_eacsl.i > example1_main_eacsl.c
26

    
27
example1_main_eacsl: example1_main_eacsl.c
28
	${GCC} -Wno-attributes -I${INC} -I. -c example1_main_eacsl.c
29
	${GCC} -I${INC} -c ${INC}/io_frontend.c
30
	${GCC} -I${INC} -c mydouble_wrapper.c
31
	${GCC} -Wno-attributes -o example1_main_eacsl io_frontend.o mydouble_wrapper.o ${FRAMACEACSL}/e_acsl.c ${FRAMACEACSL}/memory_model/e_acsl_bittree.c ${FRAMACEACSL}/memory_model/e_acsl_mmodel.c example1_main_eacsl.o 
32

    
33

    
(6-6/13)