0b55f123 |
1 | # SPIN - Verification Software - Version 5.1 - November 2007 |
2 | # |
3 | # Copyright (c) 1989-2006 Lucent Technologies, Bell Labs |
4 | # Extensions (c) 2006-2007 NASA/JPL California Institute of Technology |
5 | # All Rights Reserved. For educational purposes only. |
6 | # No guarantee whatsoever is expressed or implied by |
7 | # the distribution of this code. |
8 | # |
9 | # Written by: Gerard J. Holzmann |
10 | # Documentation: http://spinroot.com/ |
11 | # Bug-reports: bugs@spinroot.com |
12 | |
13 | CC=cc -DNXT # -DNXT enables the X operator in LTL |
14 | # CC=cc -m32 -DNXT # for 32bit compilation on a 64bit system |
15 | CFLAGS=-ansi -D_POSIX_SOURCE # on some systems add: -I/usr/include |
16 | |
17 | # for a more picky compilation: |
18 | # CFLAGS=-std=c99 -Wstrict-prototypes -pedantic -fno-strength-reduce -fno-builtin -W -Wshadow -Wpointer-arith -Wcast-qual -Winline -Wall -g |
19 | |
20 | # on PC: add -DPC to CFLAGS above |
21 | # on Solaris: add -DSOLARIS |
22 | # on MAC: add -DMAC |
23 | # on HP-UX: add -Aa |
24 | # and add $(CFLAGS) to the spin.o line: $(CC) $(CFLAGS) -c y.tab.c |
25 | # on __FreeBSD__: omit -D_POSIX_SOURCE |
26 | # also recognized: __FreeBSD__ and __OpenBSD__ and __NetBSD__ |
27 | |
28 | YACC=yacc # on Solaris: /usr/ccs/bin/yacc |
29 | YFLAGS=-v -d # creates y.output and y.tab.h |
30 | |
31 | SPIN_OS= spin.o spinlex.o sym.o vars.o main.o ps_msc.o \ |
32 | mesg.o flow.o sched.o run.o pangen1.o pangen2.o \ |
33 | pangen3.o pangen4.o pangen5.o guided.o dstep.o \ |
34 | structs.o pc_zpp.o pangen6.o reprosrc.o |
35 | |
36 | TL_OS= tl_parse.o tl_lex.o tl_main.o tl_trans.o tl_buchi.o \ |
37 | tl_mem.o tl_rewrt.o tl_cache.o |
38 | |
39 | spin: $(SPIN_OS) $(TL_OS) |
40 | $(CC) $(CFLAGS) -o spin $(SPIN_OS) $(TL_OS) |
41 | |
42 | spin.o: spin.y |
43 | $(YACC) $(YFLAGS) spin.y |
44 | $(CC) -c y?tab.c |
45 | rm -f y?tab.c |
46 | mv y?tab.o spin.o |
47 | |
48 | $(SPIN_OS): spin.h |
49 | |
50 | $(TL_OS): tl.h |
51 | |
52 | main.o pangen2.o ps_msc.o: version.h |
53 | pangen1.o: pangen1.h pangen3.h pangen6.h |
54 | pangen2.o: pangen2.h pangen4.h pangen5.h |
55 | |
56 | # http://spinroot.com/uno/ |
57 | # using uno version 2.13 -- Oct 2007 |
58 | |
59 | uno: spin.o |
60 | uno_local -picky dstep.c flow.c guided.c main.c mesg.c pangen3.c pangen4.c pangen5.c pangen6.c pc_zpp.c ps_msc.c reprosrc.c run.c sched.c spinlex.c structs.c sym.c tl_buchi.c tl_cache.c tl_lex.c tl_main.c tl_mem.c tl_parse.c tl_rewrt.c tl_trans.c vars.c |
61 | uno_local -picky pangen1.c # large includes, handle separately for now |
62 | uno_local -picky pangen2.c |
63 | rm -f spin.o y?tab.? *.uno y.output y.debug |
64 | |
65 | clean: |
66 | rm -f spin *.o y?tab.[ch] y.output y.debug |
67 | rm -f pan.[chmotb] a.out core *stackdump |
68 | |
69 | coverity: |
70 | cov-build --dir covty make |
71 | cov-translate --dir covty gcc -c *.c |
72 | cov-analyze --dir covty |
73 | cov-format-errors --dir covty -x -X |
74 | echo ./covty/output/errors/index.html |