source: vis_dev/vis-2.1/Makefile.in @ 16

Last change on this file since 16 was 11, checked in by cecile, 13 years ago

Add vis
File size: 35.6 KB
Line 
1# FileName      [ Makefile.in ]
2#
3# PackageName   [ vis ]
4#
5# Synopsis      [ Package-wide Makefile ]
6#
7# Description   [ This file requires GNU's make program.
8#                 Run "configure" to generate the Makefile, or use
9#                 "config.status" (created by configure) to regenerate the
10#                 Makefile after modifying this file.
11#
12#                 Type "gmake help" for help about valid targets.
13#                ]
14#
15# SeeAlso       [ configure.in ]
16#
17# Author        [ Stephen Edwards <sedwards@eecs.berkeley.edu>
18#                 Tom Shiple <shiple@eecs.berkeley.edu> ]
19#
20# Copyright     [
21#  Copyright (c) 1994-1996 The Regents of the Univ. of California.
22#  All rights reserved.
23#
24#  Permission is hereby granted, without written agreement and without license
25#  or royalty fees, to use, copy, modify, and distribute this software and its
26#  documentation for any purpose, provided that the above copyright notice and
27#  the following two paragraphs appear in all copies of this software.
28#
29#  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
30#  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
31#  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
32#  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
33#
34#  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
35#  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
36#  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
37#  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
38#  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
39#  ]
40#
41# Revision      [$Id: Makefile.in,v 1.124 2005/05/18 20:59:38 fabio Exp $]
42
43# Default target:
44
45.PHONY : default
46
47default : all
48
49#----------------------------------------------------------------------
50# The list of packages to compile.  Change this if you are only compiling
51# part of VIS
52#----------------------------------------------------------------------
53
54#PKGS = tst
55PKGS = $(ALL_PKGS)
56
57# The name of the BDD package to use
58
59BDDPKG =        @BDDLIB@
60
61#----------------------------------------------------------------------
62# This Makefile is designed for three different situations:
63#
64# 1. Single platform build (the default)
65#
66#    All packages listed in the PKGS variable
67#    local_srcdir = master_srcdir = .
68#
69# 2. Multi-platform build
70#
71#    All packages listed in the PKGS variable
72#    local_srcdir = master_srcdir = /where/source/files/reside
73#
74# 3. Multi-platform development (used at Berkeley)
75#
76#    Packages under development listed in the PKGS variable
77#    local_srcdir = ../common
78#    master_srcdir = /projects/vis/vis-devel/common
79#
80#    User has a directory structure that looks like
81#
82#       vis/common/src/         Subdirectory with package source files
83#                               under development.
84#
85#       vis/$PLATFORM/          Subdirectory with this Makefile.
86#                               Compilation is invoked here.
87#
88#       $PLATFORM is something like "alpha-g" (DEC Alpha, debug version)
89#
90#----------------------------------------------------------------------
91
92#----------------------------------------------------------------------
93# Information about all the packages
94#----------------------------------------------------------------------
95
96ALL_PKGS = abs amc baig bmc cmd ctlp ctlsp eqv fsm rob grab hrc imc img io ltl \
97        maig mark mc mvf mvfaig ntk ntm ntmaig ord part puresat rst res restr \
98        rt sat sim spfd synth tbl truesim tst var vm
99# Generate the list of all packages NOT in the PKGS list
100
101MISSING_PKGS = $(filter-out $(PKGS), $(ALL_PKGS))
102
103# All the BDD packages
104BDDPKGS = cu cmu cal
105
106#----------------------------------------------------------------------
107# For safety
108#----------------------------------------------------------------------
109
110SHELL = /bin/sh
111.SUFFIXES:
112
113#----------------------------------------------------------------------
114# The name of the product and its version
115#----------------------------------------------------------------------
116
117PRODUCT = vis
118VERSION = 2.1
119
120# Compile and version information
121#
122# CUR_DATE and CUR_VER are strings surrounded by double quotes that contain
123# spaces, e.g., "vis release 2.0"
124
125VERDATE := -DCUR_DATE="\"$(shell date)\"" -DCUR_VER="\"$(PRODUCT) release $(VERSION)\""
126
127#----------------------------------------------------------------------
128# Source directories
129#----------------------------------------------------------------------
130
131# Directory containing master source files.  This directory is searched
132# for packages NOT listed in the PKGS variable.  Defaults to "."
133# Override with  ./configure --srcdir=
134master_srcdir = @srcdir@
135
136# Directory containing local source files.  This directory is searched
137# for packages listed in the PKGS variable.  Defaults to the master source
138# directory (see above).
139# Override with ./configure --with-local-srcdir=
140local_srcdir =  @local_srcdir@
141
142#----------------------------------------------------------------------
143# Directories used while building
144#----------------------------------------------------------------------
145
146# Directories to search for glu .h files (space-separated)
147gluincdir1 =    @gluincdir@
148
149# Directories to search for libglu.a (space-separated)
150glulibdir1 =    @glulibdir@
151
152# Directory where object files will be placed during the build
153objectdir =     obj
154
155# Directory where links to header files will be placed during the build
156headerdir =     $(local_srcdir)/include
157
158# Directories where documentation will be placed during the build
159docdir =        $(master_srcdir)/doc
160htmldocdir =    $(docdir)/html
161txtdocdir =     $(docdir)/txt
162helpdir =       $(master_srcdir)/share/help
163
164# Directories to search for VIS library files
165# Set by ./configure --with-vis-libdir=
166vislibdir =     @vislibdir@
167
168# Full path of platform-independent library files during the build.
169# Using this variable as an environment variable allows VIS to work
170# before it is installed.
171#
172# Note: This is NOT where they will be installed
173
174VIS_LIBRARY_PATH = $(shell cd $(master_srcdir)/share ; pwd)
175
176#----------------------------------------------------------------------
177# Defaults for GLU library and header files
178#----------------------------------------------------------------------
179
180ifndef gluincdir1
181  gluincdir = ../glu-$(VERSION)/include ../../glu-$(VERSION)/include
182else
183  gluincdir = $(gluincdir1)  $(gluincdir1)/../src/cudd
184endif
185
186ifndef glulibdir1
187  glulibdir = ../glu-$(VERSION) ../../glu-$(VERSION)
188else
189  glulibdir = $(glulibdir1)
190endif
191
192#----------------------------------------------------------------------
193# Installation names and directories
194#----------------------------------------------------------------------
195
196# Name of the library to create
197LIBRARY =       lib$(PRODUCT).a
198
199# Name of the man page
200MANPAGE =       vis.1
201
202# Directory in which to install architecture-independent files
203# Set by ./configure --prefix=...
204prefix =        @prefix@
205
206# Directory in which to install architecture-dependent files
207# Set by ./configure --exec-prefix=...
208exec_prefix =   @exec_prefix@
209
210# Directory in which to install binaries
211bindir =        $(exec_prefix)/bin
212
213# Directory in which to install libraries
214libdir =        $(exec_prefix)/lib
215
216# Directory in which to install headers
217includedir =    $(prefix)/include
218
219# Directory in which to install architecture-independent library files
220datadir =       $(prefix)/share/vis
221
222# Directory for the man page
223mandir = $(prefix)/man/man1
224
225#----------------------------------------------------------------------
226# The following are set by the configure script
227#----------------------------------------------------------------------
228
229AC_FLAGS =      @DEFS@
230LIBDIRS =       @LIBDIRS@
231RANLIB =        @RANLIB@
232CC =            @CC@
233LINKER =        @LINKER@
234LDFLAGS =       @LDFLAGS@
235CPPFLAGS =      @CPPFLAGS@
236#
237# Define the linker for the executable with "memory_profile" activated
238#
239PLINKER =       @PLINKER@
240CFLAGS =        @CFLAGS@
241OTHERLIBS =     -lm @LIBS@ @LEXLIB@
242YACC =          @YACC@
243LEX =           @LEX@
244NAWK =          @AWK@
245INSTALL =       @INSTALL@
246INSTALL_PROGRAM = @INSTALL_PROGRAM@
247INSTALL_DATA =  @INSTALL_DATA@
248AR =            @AR@
249ZCHAFF=         @ZCHAFF@
250#----------------------------------------------------------------------
251# Examples included in the distribution
252#----------------------------------------------------------------------
253
254# Each example is declared only once. If some checking through is done
255# make check, then it is declared in one of CHECK_COMMON_EXAMPLES,
256# CHECK_EXAMPLES_cu, CHECK_EXAMPLES_cmu or CHECK_EXAMPLES_cu. If the example
257# is just being added to the examples directory in VIS, then add it here.
258
259EXAMPLES = $(CHECK_COMMON_EXAMPLES) $(CHECK_EXAMPLES_cu) \
260                $(CHECK_EXAMPLES_cmu) $(CHECK_EXAMPLES_cal) \
261                bpb eight_queens minmax ping_pong_new rcnum
262
263# The "interesting" example files are anything in the examples subdirectories
264# except the RCS subdirectories
265#
266# This is a rather messy way to look for filenames in the local_srcdir,
267# then remove the local_srcdir prefix
268
269EXAMPLEFILES = $(patsubst $(local_srcdir)/%, %, \
270                $(filter-out %RCS, $(foreach example, $(EXAMPLES), \
271                  $(wildcard $(local_srcdir)/examples/$(example)/*))))
272
273# $(pathsubst $(local_srcdir)/%, %, \
274#       $(filter-out %/RCS, $(foreach example, $(EXAMPLES), \
275
276
277#----------------------------------------------------------------------
278# Distributed files in the doc directory
279#----------------------------------------------------------------------
280
281DOCUMENTATION = blifmv.ps ctl.ps vis_user.ps two_phase.ps
282
283#----------------------------------------------------------------------
284# Files in the share directory
285#----------------------------------------------------------------------
286
287SHAREFILES = master.visrc ioBlifToMv.nawk ioBlifToMvForIncremental.nawk\
288             script_compute_reach.simple script_compute_reach.robust\
289             script_model_check.simple script_model_check.robust\
290             script_fair_model_check.simple script_fair_model_check.robust\
291             script_lang_empty_check.simple script_lang_empty_check.robust\
292             script_generic.simple script_generic.robust\
293             sislib.mv createfunctionmap memoryaccount visdbgpp
294
295HELPFILES = $(notdir $(wildcard $(helpdir)/*.txt))
296
297#----------------------------------------------------------------------
298# Include the make templates from all the packages
299#
300# Each of these templates (e.g., array/array.make) should contains lines
301# of the form
302#
303# CSRC += source1.c source2.c
304# HEADERS += header1.h header2.h
305# LEXSRC += file1.l
306# YACCSRC += file2.y
307# GENERATEDCSRC += ctlpLex.c ctlpRead.c
308#----------------------------------------------------------------------
309
310MAKEINCLUDES = $(foreach package, $(PKGS), \
311        $(local_srcdir)/src/$(package)/$(package).make)
312
313include $(MAKEINCLUDES)
314
315OBJECTS = $(addprefix $(objectdir)/,$(GENERATEDCSRC:.c=.o) $(CSRC:.c=.o))
316
317#----------------------------------------------------------------------
318# Include the dependency files from each package directory.
319# A missing dependency file does not produce an error.
320#----------------------------------------------------------------------
321
322DEPENDENCIES = $(foreach package, $(PKGS), \
323        $(local_srcdir)/src/$(package)/$(package).d)
324
325-include $(DEPENDENCIES)
326
327#----------------------------------------------------------------------
328# Header files and library search paths and names
329#
330# INCLUDEDIRS looks like "-I/projects/glu/ -I/projects/vis/ ..."
331# LIBRARYDIRS looks like "-L/projects/glu/ -L/projects/vis/ ..."
332# LIBS looks like "-lm -lglu -lvis"
333#----------------------------------------------------------------------
334
335INCLUDEDIRS = $(addprefix -I,$(gluincdir)) \
336                $(foreach package, $(PKGS), -I$(local_srcdir)/src/$(package)) \
337                $(foreach package, $(MISSING_PKGS), \
338                -I$(master_srcdir)/src/$(package)) \
339                -I$(objectdir) \
340                $(CPPFLAGS)
341
342LIBRARYDIRS = $(addprefix -L,$(vislibdir)) $(addprefix -L,$(glulibdir)) \
343                $(LIBDIRS)
344
345# Link against the VIS library only if some packages are missing
346# (i.e., we are compiling only a few packages locally)
347
348ifneq ($(strip $(MISSING_PKGS)),)
349  VISLIBS = -l$(PRODUCT)
350else
351  VISLIBS =
352endif
353
354GLULIBS = -l$(BDDPKG) -lglu
355
356# g++ on Linux RH requires -lstdc++
357ifeq ($(CC),g++)
358OTHERLIBS += -lstdc++
359endif
360
361LIBS = $(VISLIBS) $(GLULIBS) $(OTHERLIBS)
362
363#----------------------------------------------------------------------
364# Form the the list of directories to search for header files.
365#
366# VPATH looks like /projects/vis:/projects/glu/: ...
367#----------------------------------------------------------------------
368
369VPATH = $(local_srcdir): \
370        $(master_srcdir): \
371        $(addprefix :$(local_srcdir)/src/,$(PKGS)): \
372        $(addprefix :$(master_srcdir)/src/,$(MISSING_PKGS)): \
373        $(objectdir): \
374        $(local_srcdir)/share
375
376#----------------------------------------------------------------------
377# Definitions for the distribution file
378#----------------------------------------------------------------------
379
380DISTRIBUTION = $(PRODUCT)-$(VERSION)
381
382# Directories to include in the distribution file
383
384DISTDIRS = src helpers share share/help obj doc examples \
385        $(addprefix examples/,$(EXAMPLES)) $(addprefix src/,$(PKGS))
386
387# Build/install helper files
388
389HELPERS = $(addprefix helpers/, \
390        install-sh mkinstalldirs config.guess config.sub dependency.make)
391
392# Files to include in the distribution file
393
394DISTFILES = \
395        README INSTALL NEWS \
396        configure configure.in Makefile.in $(HELPERS) \
397        vis.1 \
398        xsimv \
399        $(CSRC) $(HEADERS) $(LEXSRC) $(YACCSRC) $(MAKEINCLUDES) \
400        $(EXAMPLEFILES) \
401        $(addprefix doc/,$(DOCUMENTATION)) \
402        $(addprefix share/,$(SHAREFILES)) \
403        $(addprefix share/help/,$(HELPFILES))
404
405#----------------------------------------------------------------------
406# Variables used by for Revision Control
407#----------------------------------------------------------------------
408
409# The root RCS directory
410rcs_rootdir          = /projects/vis/rcsRoot/common
411
412RCSFILES        = $(CSRC) $(HEADERS) $(LEXSRC) $(YACCSRC) $(MAKEINCLUDES)
413
414RCSMISCFILES      = Makefile.in configure.in localconfigure \
415        masterconfigure README INSTALL NEWS xsimv $(addprefix helpers/, mkinstalldirs install-sh \
416                config.guess config.sub dependency.make )
417
418RCSSHAREFILES        = $(SHAREFILES)
419
420#----------------------------------------------------------------------
421# Implicit rules
422#----------------------------------------------------------------------
423
424ALLCFLAGS = $(CFLAGS) $(AC_FLAGS) $(VERDATE) \
425                -DNAWK=\"$(NAWK)\" -DLIBRARY=\"$(datadir)\"
426
427# For compiling a source file into the object directory
428
429$(objectdir)/%.o : %.c
430        umask 2 ; $(CC) -c $(ALLCFLAGS) $(INCLUDEDIRS) -o $@ $<
431
432# Place object files into an archive
433
434%.a :
435        rm -f $@
436        umask 2; $(AR) cq $@ $^
437        $(RANLIB) $@
438
439######################################################################
440#                               RULES                                #
441######################################################################
442
443#:
444#: Useful targets:
445#:
446
447#----------------------------------------------------------------------
448# Rule for getting help
449#----------------------------------------------------------------------
450
451.PHONY : help
452
453#: help -- Print a list of targets
454
455# This prints all lines in this Makefile that begin with #:
456
457help :
458        @sed -n "s/^#://p" Makefile
459
460#----------------------------------------------------------------------
461# Always executed once when the Makefile is run
462#----------------------------------------------------------------------
463
464# Make sure the directory in which to place the objects exists
465
466ignored := $(shell umask 2; test -d $(objectdir) || mkdir $(objectdir))
467
468#----------------------------------------------------------------------
469# Rules to compile and build libraries and executables
470#----------------------------------------------------------------------
471
472.PHONY : all allprods library allprods-mp exe-mp compile-version delete-version
473
474#:
475#: all (the default) -- Compile the main executable
476# (force the version to be recompiled)
477
478all : ALLCFLAGS += -DBDD$(BDDPKG)
479
480all : compile-version $(PRODUCT)
481
482# Create the main executable
483$(PRODUCT) : $(OBJECTS) $(glulibdir)/libglu.a $(glulibdir)/lib$(BDDPKG).a
484        umask 2 ; $(LINKER) -o $(PRODUCT) $(LDFLAGS) \
485                $(OBJECTS) $(LIBRARYDIRS) $(LIBS)
486
487#: allprods -- Compile an executable linked with each BDD package
488
489allprods : $(OBJECTS) $(glulibdir)/libglu.a $(foreach bddpkg, $(BDDPKGS), \
490           $(glulibdir)/lib$(bddpkg).a)
491        @for bddpkg in $(BDDPKGS) ; \
492        do \
493          rm -f $(objectdir)/satBDD.o; \
494          umask 2 ; $(CC) -c $(ALLCFLAGS) -DBDD$$bddpkg $(INCLUDEDIRS) -o $(objectdir)/satBDD.o  $(master_srcdir)/src/sat/satBDD.c; \
495          echo "Creating vis-$$bddpkg";\
496          umask 2 ; $(LINKER) -o $(PRODUCT)-$$bddpkg $(LDFLAGS) $(OBJECTS) \
497                $(LIBRARYDIRS) $(VISLIBS) -l$$bddpkg -lglu $(OTHERLIBS); \
498        done
499
500# Force the "version" information to be recompiled
501
502compile-version : delete-version $(objectdir)/vmVers.o $(objectdir)/satBDD.o
503
504# Delete the object file related to the version
505
506delete-version :
507        rm -f $(objectdir)/vmVers.o $(objectdir)/satBDD.o
508
509# Build a library containing all the objects
510
511#: library -- Create a library of all the objects (useful in a central area)
512
513library : $(LIBRARY)
514
515$(LIBRARY) : $(OBJECTS)
516
517ifdef PLINKER
518$(PRODUCT)-mp : $(LIBRARY) $(glulibdir)/libglu.a \
519                $(foreach bddpkg, $(BDDPKGS), \
520                $(glulibdir)/lib$(bddpkg).a)
521        umask 2 ; $(PLINKER) -o $(PRODUCT)-mp $(OBJECTS) \
522                `purify -printhomedir`/libpurify_stubs.a \
523                $(LIBRARYDIRS) $(LIBS)
524
525allprods-mp : $(LIBRARY) $(glulibdir)/libglu.a \
526                $(foreach bddpkg, $(BDDPKGS), \
527                $(glulibdir)/lib$(bddpkg).a)
528        @for bddpkg in $(BDDPKGS) ; \
529        do \
530          echo "Creating vis-$$bddpkg";\
531          umask 2 ; $(PLINKER) -o $(PRODUCT)-$$bddpkg-mp $(OBJECTS) \
532                `purify -printhomedir`/libpurify_stubs.a \
533                $(LIBRARYDIRS) $(VISLIBS) -l$$bddpkg -lglu $(OTHERLIBS) ; \
534        done
535
536exe-mp : $(OBJECTS)
537        $(PLINKER) -o $(PRODUCT)-mp $(OBJECTS) \
538                `purify -printhomedir`/libpurify_stubs.a \
539                $(LIBRARYDIRS) $(LIBS)
540endif
541
542#----------------------------------------------------------------------
543# Rule to produce the function map for the memory_profile command
544#----------------------------------------------------------------------
545
546.PHONY : functionmap
547
548FMAPFILE = .fmap
549functionmap: $(CSRC)
550        $(VIS)/common/share/createfunctionmap $^ >$(FMAPFILE)
551
552#----------------------------------------------------------------------
553# Rules for installation
554#----------------------------------------------------------------------
555
556.PHONY : install uninstall installdirs
557
558#:
559#: install -- Install the product and libraries in bindir, libdir,
560#:            datadir, etc.
561
562install : $(PRODUCT) $(LIBRARY) installdirs
563        @echo "Installing $(bindir)/$(PRODUCT)"
564        @$(INSTALL_PROGRAM) $(PRODUCT) $(bindir)/$(PRODUCT)
565        @echo "Installing $(libdir)/$(LIBRARY)"
566        @$(INSTALL_DATA) $(LIBRARY) $(libdir)/$(LIBRARY)
567        @for file in $(SHAREFILES) ; do \
568                echo "Installing $(datadir)/$$file"; \
569                $(INSTALL_DATA) $(master_srcdir)/share/$$file \
570                        $(datadir)/$$file; \
571        done
572        @for file in $(HELPFILES) ; do \
573                echo "Installing $(datadir)/help/$$file"; \
574                $(INSTALL_DATA) $(master_srcdir)/share/help/$$file \
575                        $(datadir)/help/$$file; \
576        done
577        @echo "Installing $(mandir)/vis.1"
578        @$(INSTALL_DATA) vis.1 $(mandir)/vis.1
579        @for header in $(HEADERS); do \
580                echo "Installing $(includedir)/$$header"; \
581                $(INSTALL_DATA) $(master_srcdir)/src/*/$$header \
582                        $(includedir)/$$header; \
583        done
584
585#: uninstall -- Reverse the effects of "install"
586
587uninstall :
588        rm -f $(bindir)/$(PRODUCT)     
589        rm -f $(libdir)/$(LIBRARY)
590        @for file in $(SHAREFILES) ; \
591        do \
592          echo "Removing $(datadir)/$$file"; \
593          rm -f $(datadir)/$$file; \
594        done
595        @for file in $(HELPFILES) ; \
596        do \
597          echo "Removing $(datadir)/help/$$file"; \
598          rm -f $(datadir)/help/$$file; \
599        done
600        @for header in $(HEADERS); \
601        do \
602          echo "Removing $(includedir)/$$header"; \
603          rm -f $(includedir)/$$header; \
604        done
605
606installdirs :
607        $(master_srcdir)/helpers/mkinstalldirs \
608                $(bindir) $(libdir) $(includedir) $(datadir) $(datadir)/help \
609                $(mandir)
610
611#----------------------------------------------------------------------
612# Rules for checking the build
613#----------------------------------------------------------------------
614
615.PHONY : check check-examples
616
617# This is a lengthy sed command used to filter out the irrelevant VIS
618# output that appears when the examples are running.
619#
620# Sed does not permit space between the trailing p ("print matching
621# lines") and the semicolon (end of command).  Hashes are escaped --
622# otherwise they are Makefile comments.  This was once a long egrep
623# expression, but the string was too long for Ultrix's egrep.
624
625SED_CMD = \
626        /^FSM depth/p; \
627        /^computation depth/p; \
628        /^reachable states =/p; \
629        /^\# MC: formula passed/p; \
630        /^\# MC: formula failed/p; \
631        /^\# MC: the number of non-trivial forced segments/p; \
632        /^\# MC: Vacuous/p; \
633        /^\# MC: No vacuous/p; \
634        /[sS]tates covered/p; \
635        /covered states/p; \
636        /Percentage of coverage/p; \
637        /^\# LTL_MC: formula passed/p; \
638        /^\# LTL_MC: formula failed/p; \
639        /^\# INV: formula passed/p; \
640        /^\# INV: formula failed/p; \
641        /^\# LE: language is not empty/p; \
642        /^\# LE: language emptiness check passes/p; \
643        /^\# ABS: formula passed/p; \
644        /^\# ABS: formula failed/p; \
645        /^\# BMC: formula failed/p;\
646        /^\# BMC: no counterexample found/p; \
647        /Residue/p; \
648        /^\# AMC: Verified formula TRUE/p; \
649        /^\# AMC: Verified formula FALSE/p; \
650        /Equivalence Classes/p; \
651        /Total number of literals/p; \
652        /Networks are combinationally equivalent\./p; \
653        /Networks are sequentially equivalent\./p; \
654        /;.*;/p;
655
656CHECK_EXAMPLES_cu = daio_receiver mult6x6 s1269 fpmpy restruct synthesis \
657        production_cell
658CHECK_EXAMPLES_cmu =
659CHECK_EXAMPLES_cal =
660
661# List of all examples to check (A subset of EXAMPLES)
662
663CHECK_COMMON_EXAMPLES = abp amp arbiter bakery coherence counter crd ctlp3 \
664        dcnew eisenberg elevator ethernet exampleS gcd gigamax ping_pong \
665        scheduler short slider tbl_one_bug tcp tlc treearbiter
666
667CHECK_EXAMPLES = $(CHECK_COMMON_EXAMPLES) $(CHECK_EXAMPLES_$(BDDPKG))
668
669# Determine the absolute executable path
670#
671# Starting from the current directory, change directory to the directory
672# part of the product name, then tack on the filename part of EXECUTABLE
673
674EXECUTABLE = $(PRODUCT)
675
676EXECUTABLEPATH := \
677        $(shell cd $(dir $(EXECUTABLE)) ; pwd)/$(notdir $(EXECUTABLE))
678
679# Determine the rootname of the examples
680#
681
682EXAMPLEPATH = $(master_srcdir)/examples
683
684FULLEXAMPLEPATH := $(shell cd $(EXAMPLEPATH) ; pwd)
685
686#:
687#: check -- Test the locally-built executable (runs check-examples)
688
689check : check-examples
690
691# Run check on each of the bdd versions (named e.g., vis-cmu)
692
693#: check-allprods -- Test each of the BDD executables (see allprods)
694
695check-allprods :
696        @for bddpkg in $(BDDPKGS) ; \
697        do \
698          echo "Checking $(PRODUCT)-$$bddpkg";\
699          $(MAKE) PRODUCT=$(PRODUCT)-$$bddpkg BDDPKG=$$bddpkg check ; \
700        done
701
702#: check-examples -- Test each of the examples listed in CHECK_EXAMPLES
703#:          You may want to invoke this with
704#:            gmake "CHECK_EXAMPLES=abp bakery" check-examples
705#:            gmake EXECUTABLE=vis-cmu check-examples
706#:            gmake EXECUTABLE=/projects/vis/vis-devel/alpha-g/vis \
707#:                    check-examples
708#:            gmake EXAMPLEPATH=/projects/vis/vis-devel/common/examples \
709#:                    check-examples
710#:            gmake EXAMPLEPATH=../common/examples check-examples
711#:            gmake VIS_LIBRARY_PATH=/projects/vis/vis-devel/share
712
713# For each example,
714#
715# 1) create the directory checkresults/<example>
716# 2) enter that directory
717# 3) create "check_script" by prepending a "set open_path" command
718#    to the example's check_script in the master source directory.  This
719#    makes VIS look in the master source directory for example files
720# 4) run VIS on that script, producing "result.raw"
721# 5) filter out relevant lines in the result, producing "result.filtered"
722#    and compare this with the "check_result" file in the master source
723#    directory.  Differences are written to "result.differences"
724
725check-examples :
726        @test -d checkresults || mkdir checkresults
727        @echo "Checking examples.  Results will be in checkresults/<example>/result.raw"
728        @echo "Running executable $(EXECUTABLEPATH)"
729        @echo " (change with EXECUTABLE=...)"
730        @echo "Taking examples from $(FULLEXAMPLEPATH)"
731        @echo " (change with EXAMPLEPATH=...)"
732        @cwd=`pwd` ; \
733        VIS_LIBRARY_PATH=$(VIS_LIBRARY_PATH) ; \
734        export VIS_LIBRARY_PATH ; \
735        for example in $(CHECK_EXAMPLES) ; \
736        do \
737          echo -n "Checking $$example ... " ; \
738          cd $$cwd ; \
739          test -d checkresults/$$example || \
740                mkdir checkresults/$$example ; \
741          cd checkresults/$$example ; \
742          rm -f check_script ; \
743          echo "set open_path $(FULLEXAMPLEPATH)/$$example" > check_script ; \
744          cat $(FULLEXAMPLEPATH)/$$example/check_script >> check_script ; \
745          $(EXECUTABLEPATH) -f check_script -x > result.raw 2> result.stderr ; \
746          sed -n '$(SED_CMD)' result.raw > result.filtered ; \
747          if diff result.filtered \
748                $(FULLEXAMPLEPATH)/$$example/check_result > result.differences ; \
749          then \
750            echo "passed" ; \
751            rm result.differences ; \
752          else \
753            echo "failed (more checkresults/$$example/result.differences)" ; \
754          fi ; \
755        done
756
757#         egrep '$(KEY_WORDS)' result.raw > result.filtered ; \
758
759#----------------------------------------------------------------------
760# Rules that produce/delete the dependency file for every package
761#----------------------------------------------------------------------
762
763.PHONY : dependencies cleandependencies
764
765#:
766#: dependencies -- Create a list of dependency files.
767#:                 Useful when modifying header files.
768
769# Invoke the "dependency.make" Makefile on each package subdirectory,
770# passing the path, etc. to it.
771#
772# There's a strange feature in autoconf where lines of the form " VPATH="
773# are removed from the Makefile.  Thus, a flag is placed before the
774# VPATH= argument below.
775
776dependencies:
777ifneq ($(findstring <$(CC)>,<gcc> <g++>),)
778        for pkg in $(PKGS) ; \
779        do \
780          $(MAKE) --no-print-directory \
781                -f $(master_srcdir)/helpers/dependency.make \
782                CC="$(CC)" \
783                CFLAGS="$(CFLAGS)" VPATH="$(local_srcdir)/src/$$pkg" \
784                AC_FLAGS="$(AC_FLAGS)" \
785                INCLUDEDIRS="$(INCLUDEDIRS)" objectdir=$(objectdir) \
786                PKGNAME=$(local_srcdir)/src/$$pkg/$$pkg \
787                $(local_srcdir)/src/$$pkg/$$pkg.d ; \
788        done
789else
790        @echo "dependency requires gcc or g++"
791        @echo "Reconfigure with gcc or g++"
792endif
793
794cleandependencies:
795        rm -f $(local_srcdir)/src/*/*.d
796
797#----------------------------------------------------------------------
798# Rules for making a distribution file
799#----------------------------------------------------------------------
800
801.PHONY : dist
802
803#:
804#: dist -- Create a tarred, gzipped distribution file
805
806# Warning: "tar" under Digital Unix (on DEC Alphas) writes directories
807# that don't work under SunOS tar
808
809dist : $(DISTRIBUTION).tar.gz
810
811$(DISTRIBUTION).tar.gz : $(DISTFILES)
812ifeq ($(strip $(FULL_MISSING_PKGS)),)
813        rm -rf $(DISTRIBUTION)
814        umask 022; mkdir $(DISTRIBUTION)
815        for dir in $(DISTDIRS); \
816        do \
817          umask 022; mkdir $(DISTRIBUTION)/$$dir; \
818        done
819        @echo "Copying distribution files"
820        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
821        do \
822          echo "  $$file"; \
823          cp -p $(local_srcdir)/$$file $(DISTRIBUTION)/$$file; \
824        done
825        - chmod -R a+r $(DISTRIBUTION)
826        - chmod -R u+w $(DISTRIBUTION)
827        tar cf - $(DISTRIBUTION) | gzip -9 > $(DISTRIBUTION).tar.gz
828        rm -rf $(DISTRIBUTION)
829else
830        @echo "Missing packages: $(FULL_MISSING_PKGS)"
831        @echo "Make sure PKGS lists all the packages"
832        @exit 1
833endif
834
835#----------------------------------------------------------------------
836# Rules for rebuilding the configure file and Makefile
837#----------------------------------------------------------------------
838
839${master_srcdir}/configure : configure.in
840        cd ${master_srcdir} && autoconf
841        chmod 0775 ${master_srcdir}/config*
842
843config.status : configure
844        ./config.status --recheck
845
846Makefile : Makefile.in config.status
847        @echo "The master Makefile.in has been changed:"
848        @echo "run config.status"
849        @echo "Warning: This will overwrite any local Makefile modifications"
850        @exit 1
851
852#----------------------------------------------------------------------
853# Rules for cleaning
854#----------------------------------------------------------------------
855
856.PHONY : clean mostlyclean distclean
857
858#:
859#: clean -- Remove every file created by building
860
861clean mostlyclean :
862        rm -rf $(objectdir)/* $(LIBRARY) $(PRODUCT) \
863                $(foreach bddpkg, $(BDDPKGS), $(PRODUCT)-$(bddpkg)) \
864                checkresults include
865
866#: distclean -- Remove every file created by building or configuring
867
868distclean : clean cleandependencies
869        rm -f Makefile config.status config.cache config.log
870
871#----------------------------------------------------------------------
872# Rule for performing a lint-like check on the source code
873#
874# Note: This requires gcc or g++
875#----------------------------------------------------------------------
876
877.PHONY : check-code
878
879#:
880#: check-code -- Run a lint-like check on the source code.
881#:               (useful for development)
882
883CHECK_FLAGS := -Wall -pedantic -DBDD$(BDDPKG)
884ifeq ($(CC),gcc)
885  CHECK_FLAGS += -Wstrict-prototypes -Wmissing-prototypes -Wmissing-declarations
886endif
887
888check-code : $(CSRC) $(BDD_CSRC) $(MDD_CSRC)
889ifneq ($(findstring <$(CC)>,<gcc> <g++>),)
890        @rm -f *.o_checkcode
891        @for file in $^; \
892        do \
893          echo "------------------------ Checking $$file"; \
894          $(CC) -c $(CFLAGS) $(AC_FLAGS) $(CHECK_FLAGS) \
895                $(VERDATE) $(INCLUDEDIRS) \
896                -o $(objectdir)/checkcode_output.o $$file; \
897          rm -f $(objectdir)/checkcode_output.o; \
898        done
899        @rm -f *.o_checkcode
900else
901        @echo "check-code requires gcc or g++"
902        @echo "Reconfigure with gcc or g++"
903endif
904
905#----------------------------------------------------------------------
906# Rule for generating function prototypes for all the
907# source and header files in all the PKGS
908#
909# Note: This requires "extproto," part of the ext package available from
910# ftp://ic.eecs.berkeley.edu/pub/Ext
911#----------------------------------------------------------------------
912
913.PHONY : proto
914
915#:
916#: proto -- Regenerate all the function prototypes in the packages
917#:          Useful during development.  You may want to invoke it with
918#:            gmake "PKGS=tst tbl" proto
919
920proto :
921        @cd $(local_srcdir)/src ; \
922        for pkg in $(PKGS); \
923        do \
924          cd $$pkg ; \
925          extproto *.h *.c ; \
926          cd .. ; \
927        done
928
929#----------------------------------------------------------------------
930# Rules for generating the documentation and command help files
931# for all the packages
932#
933# Note: This requires "extdoc," part of the ext package, and
934# lynx, a textual WWW browser
935#----------------------------------------------------------------------
936
937.PHONY : allDoc doc indices helpfiles cleandoc
938
939#:
940#: allDoc -- Extract all the documentation (runs doc, indices, and helpfiles)
941
942allDoc : cleandoc doc indices helpfiles
943
944#: doc -- Extract HTML and text documentation on all the functions
945
946doc : $(htmldocdir) $(txtdocdir)
947        for pkg in $(PKGS); \
948        do \
949          umask 2 ; extdoc --html=$(htmldocdir) --text=$(txtdocdir) \
950                $(local_srcdir)/src/$$pkg/$$pkg; \
951        done
952
953#: indices -- Generate function and command indices for the HTML documentation
954
955indices : $(htmldocdir)
956        umask 2 ; extindex $(htmldocdir)
957
958#: helpfiles -- Generate the help files from the HTML documentation
959
960helpfiles : $(helpdir)
961        for file in $(htmldocdir)/*Cmd.html ; \
962        do \
963          echo Converting $$file ; \
964          umask 2 ; lynx -dump $$file > $(helpdir)/`basename $$file .html`.txt ; \
965        done
966
967#: cleandoc -- Remove all the documentation generated by "allDoc"
968
969cleandoc :
970        -rm -f $(htmldocdir)/*.html
971        -rm -f $(txtdocdir)/*.txt
972        -rm -f $(helpdir)/*Cmd.txt
973
974$(htmldocdir) :
975        - umask 2 ; mkdir $(htmldocdir)
976
977$(txtdocdir) :
978        - umask 2 ; mkdir $(txtdocdir)
979
980$(helpdir) :
981        - umask 2 ; mkdir $(helpdir)
982
983
984#----------------------------------------------------------------------
985# Revision control rules
986#
987# May be invoked with command-line overrides, e.g.,
988# gmake RCSFILES=foo.c rcs_co
989# gmake PKGS=array rcs_ci
990#----------------------------------------------------------------------
991
992.PHONY: rcs_ci rcs_co rcs_diff rcs_ident rcs_status
993
994#:
995#:       You may want to invoke the RCS rules with
996#:         gmake "PKGS=tst tbl" rcs_ci
997#:         gmake "RCSFILES=tstMain.c" rcs_co
998#:
999#: rcs_ci -- check in user-modified files and put an updated copy
1000#:           in the central area
1001
1002rcs_ci: $(RCSFILES)
1003        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1004        do \
1005          ci -u $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1006          co -u $(RCSFLAGS) $(master_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1007        done
1008
1009#: rcs_co -- check out files for modification
1010
1011rcs_co: $(RCSFILES)
1012        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1013        do \
1014          co -l $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1015        done
1016
1017#: rcs_diff -- Report differences between local files and checked-in versions
1018
1019rcs_diff: $(RCSFILES)
1020        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1021        do \
1022          rcsdiff $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1023        done
1024
1025#: rcs_ident -- Print the RCS identifier in each file
1026
1027rcs_ident: $(RCSFILES)
1028        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1029        do \
1030          ident $(RCSFLAGS) $(local_srcdir)/$$file; \
1031        done
1032
1033#: rcs_status -- Report who has checked out files
1034
1035rcs_status: $(RCSFILES)
1036        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1037        do \
1038          rlog -L -h $(RCSFLAGS) $(rcs_rootdir)/$$file,v; \
1039        done
1040
1041#----------------------------------------------------------------------
1042# RCS rules for common/{Makefile.in, configure.in, localconfigure,
1043# masterconfigure, mkinstalldirs, install-sh}
1044#----------------------------------------------------------------------
1045
1046.PHONY : rcs_ci_misc rcs_co_misc rcs_diff_misc
1047
1048#: rcs_ci_misc -- Check in miscellaneous files, updating central area
1049
1050rcs_ci_misc: $(RCSMISCFILES)
1051        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1052        do \
1053          ci -u $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1054          co -u $(RCSFLAGS) $(master_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1055        done
1056
1057#: rcs_co_misc -- Check out miscellaneous files
1058
1059rcs_co_misc: $(RCSMISCFILES)
1060        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1061        do \
1062          co -l $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1063        done
1064
1065#: rcs_diff_misc -- Report differences in miscellaneous files
1066
1067rcs_diff_misc: $(RCSMISCFILES)
1068        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1069        do \
1070          rcsdiff $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1071        done
1072
1073#: rcs_ident_misc -- Report RCS identifiers
1074
1075rcs_ident_misc: $(RCSMISCFILES)
1076        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1077        do \
1078          ident $(RCSFLAGS) $(local_srcdir)/$$file; \
1079        done
1080
1081#: rcs_status_misc -- Report checked in/out status, ownership
1082
1083rcs_status_misc: $(RCSMISCFILES)
1084        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1085        do \
1086          rlog -L -h $(RCSFLAGS) $(rcs_rootdir)/$$file,v; \
1087        done
1088
1089#----------------------------------------------------------------------
1090# RCS rules for files in common/share
1091#----------------------------------------------------------------------
1092
1093.PHONY : rcs_ci_share rcs_co_share rcs_diff_share
1094
1095#: rcs_ci_share -- Check in files in the share/ directory
1096
1097rcs_ci_share: $(RCSSHAREFILES)
1098        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1099        do \
1100          ci -u $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1101          co -u $(RCSFLAGS) $(master_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1102        done
1103
1104#: rcs_co_share -- Check out share files
1105
1106rcs_co_share: $(RCSSHAREFILES)
1107        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1108        do \
1109          co -l $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1110        done
1111
1112#: rcs_diff_share -- Report differences in share files
1113
1114rcs_diff_share: $(RCSSHAREFILES)
1115        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1116        do \
1117          rcsdiff $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1118        done
1119
1120#: rcs_ident_share -- Report RCS identifiers
1121
1122rcs_ident_share: $(RCSSHAREFILES)
1123        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1124        do \
1125          ident $(RCSFLAGS) $(local_srcdir)/$$file; \
1126        done
1127
1128#: rcs_status_share -- Report checked in/out status, ownership
1129
1130rcs_status_share: $(RCSSHAREFILES)
1131        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1132        do \
1133          rlog -L -h $(RCSFLAGS) $(rcs_rootdir)/$$file,v; \
1134        done
1135
1136#----------------------------------------------------------------------
1137# Rules for debugging the Makefile
1138#----------------------------------------------------------------------
1139
1140.PHONY : debug-make
1141
1142DEBUG_VARS =    ALL_PKGS \
1143                PKGS \
1144                MISSING_PKGS \
1145                VPATH \
1146                INCLUDEDIRS \
1147                CSRC \
1148                OBJECTS \
1149                HEADERS \
1150                MAKEINCLUDES \
1151                CFLAGS \
1152                AC_FLAGS \
1153                master_srcdir \
1154                local_srcdir \
1155                RCSFILES \
1156                RCSDIR \
1157                LIBS \
1158                VISLIBS \
1159                DISTFILES \
1160                EXAMPLEFILES
1161
1162#:
1163#: debug-make -- Print a list of Makefile variables
1164
1165debug-make:
1166        @$(foreach var, $(DEBUG_VARS), echo $(var)=$($(var)) ; )
Note: See TracBrowser for help on using the repository browser.