| 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 |
projects / lttv.git / blame