| 1 | # SPIN - Verification Software - Version 5.2 - September 2009 |
|---|
| 2 | # |
|---|
| 3 | # Copyright (c) 1989-2006 Lucent Technologies, Bell Labs |
|---|
| 4 | # Extensions (c) 2006-2009 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=gcc -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 -Wno-format-security -DMAC -DCPP="\"gcc -E -x c -xassembler-with-cpp\"" # 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-analyze --dir covty |
|---|
| 72 | cov-format-errors --dir covty -x -X --emacs-style > cov.out |
|---|
| 73 | |
|---|
| 74 | p10: |
|---|
| 75 | P10_R1 --dir covty --force --no-watchdog |
|---|
| 76 | P10_R2 --dir covty --force --no-watchdog --append |
|---|
| 77 | P10_R3 --dir covty --force --no-watchdog --append |
|---|
| 78 | P10_R4 --dir covty --force --no-watchdog --append |
|---|
| 79 | P10_R5 --dir covty --force --no-watchdog --append |
|---|
| 80 | P10_R9 --dir covty --force --no-watchdog --append |
|---|
| 81 | cov-format-errors --dir covty -x -X --emacs-style > p10.out |
|---|
