verif/Spin/Src5.1.6/makefile

   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