source: vis_dev/vis-2.3/Makefile.in @ 26

Last change on this file since 26 was 15, checked in by cecile, 13 years ago

Vis main file for expermeriments
File size: 35.5 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.127 2010/04/09 23:06:15 hsv 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.3
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@
235#
236# Define the linker for the executable with "memory_profile" activated
237#
238PLINKER =       @PLINKER@
239CFLAGS =        @CFLAGS@
240OTHERLIBS =     -lm @LIBS@ @LEXLIB@
241YACC =          @YACC@
242LEX =           @LEX@
243NAWK =          @AWK@
244INSTALL =       @INSTALL@
245INSTALL_PROGRAM = @INSTALL_PROGRAM@
246INSTALL_DATA =  @INSTALL_DATA@
247AR =            @AR@
248ZCHAFF=         @ZCHAFF@
249#----------------------------------------------------------------------
250# Examples included in the distribution
251#----------------------------------------------------------------------
252
253# Each example is declared only once. If some checking through is done
254# make check, then it is declared in one of CHECK_COMMON_EXAMPLES,
255# CHECK_EXAMPLES_cu, CHECK_EXAMPLES_cmu or CHECK_EXAMPLES_cu. If the example
256# is just being added to the examples directory in VIS, then add it here.
257
258EXAMPLES = $(CHECK_COMMON_EXAMPLES) $(CHECK_EXAMPLES_cu) \
259                $(CHECK_EXAMPLES_cmu) $(CHECK_EXAMPLES_cal) \
260                bpb eight_queens minmax ping_pong_new rcnum
261
262# The "interesting" example files are anything in the examples subdirectories
263# except the RCS subdirectories
264#
265# This is a rather messy way to look for filenames in the local_srcdir,
266# then remove the local_srcdir prefix
267
268EXAMPLEFILES = $(patsubst $(local_srcdir)/%, %, \
269                $(filter-out %RCS, $(foreach example, $(EXAMPLES), \
270                  $(wildcard $(local_srcdir)/examples/$(example)/*))))
271
272# $(pathsubst $(local_srcdir)/%, %, \
273#       $(filter-out %/RCS, $(foreach example, $(EXAMPLES), \
274
275
276#----------------------------------------------------------------------
277# Distributed files in the doc directory
278#----------------------------------------------------------------------
279
280DOCUMENTATION = blifmv.ps ctl.ps vis_user.ps two_phase.ps
281
282#----------------------------------------------------------------------
283# Files in the share directory
284#----------------------------------------------------------------------
285
286SHAREFILES = master.visrc ioBlifToMv.nawk ioBlifToMvForIncremental.nawk\
287             script_compute_reach.simple script_compute_reach.robust\
288             script_model_check.simple script_model_check.robust\
289             script_fair_model_check.simple script_fair_model_check.robust\
290             script_lang_empty_check.simple script_lang_empty_check.robust\
291             script_generic.simple script_generic.robust\
292             sislib.mv createfunctionmap memoryaccount visdbgpp
293
294HELPFILES = $(notdir $(wildcard $(helpdir)/*.txt))
295
296#----------------------------------------------------------------------
297# Include the make templates from all the packages
298#
299# Each of these templates (e.g., array/array.make) should contains lines
300# of the form
301#
302# CSRC += source1.c source2.c
303# HEADERS += header1.h header2.h
304# LEXSRC += file1.l
305# YACCSRC += file2.y
306# GENERATEDCSRC += ctlpLex.c ctlpRead.c
307#----------------------------------------------------------------------
308
309MAKEINCLUDES = $(foreach package, $(PKGS), \
310        $(local_srcdir)/src/$(package)/$(package).make)
311
312include $(MAKEINCLUDES)
313
314OBJECTS = $(addprefix $(objectdir)/,$(GENERATEDCSRC:.c=.o) $(CSRC:.c=.o))
315
316#----------------------------------------------------------------------
317# Include the dependency files from each package directory.
318# A missing dependency file does not produce an error.
319#----------------------------------------------------------------------
320
321DEPENDENCIES = $(foreach package, $(PKGS), \
322        $(local_srcdir)/src/$(package)/$(package).d)
323
324-include $(DEPENDENCIES)
325
326#----------------------------------------------------------------------
327# Header files and library search paths and names
328#
329# INCLUDEDIRS looks like "-I/projects/glu/ -I/projects/vis/ ..."
330# LIBRARYDIRS looks like "-L/projects/glu/ -L/projects/vis/ ..."
331# LIBS looks like "-lm -lglu -lvis"
332#----------------------------------------------------------------------
333
334INCLUDEDIRS = $(addprefix -I,$(gluincdir)) \
335                $(foreach package, $(PKGS), -I$(local_srcdir)/src/$(package)) \
336                $(foreach package, $(MISSING_PKGS), \
337                -I$(master_srcdir)/src/$(package)) \
338                -I$(objectdir)
339
340LIBRARYDIRS = $(addprefix -L,$(vislibdir)) $(addprefix -L,$(glulibdir)) \
341                $(LIBDIRS)
342
343# Link against the VIS library only if some packages are missing
344# (i.e., we are compiling only a few packages locally)
345
346ifneq ($(strip $(MISSING_PKGS)),)
347  VISLIBS = -l$(PRODUCT)
348else
349  VISLIBS =
350endif
351
352GLULIBS = -l$(BDDPKG) -lglu
353
354# g++ on Linux RH requires -lstdc++
355ifeq ($(CC),g++)
356OTHERLIBS += -lstdc++
357endif
358
359LIBS = $(VISLIBS) $(GLULIBS) $(OTHERLIBS)
360
361#----------------------------------------------------------------------
362# Form the the list of directories to search for header files.
363#
364# VPATH looks like /projects/vis:/projects/glu/: ...
365#----------------------------------------------------------------------
366
367VPATH = $(local_srcdir): \
368        $(master_srcdir): \
369        $(addprefix :$(local_srcdir)/src/,$(PKGS)): \
370        $(addprefix :$(master_srcdir)/src/,$(MISSING_PKGS)): \
371        $(objectdir): \
372        $(local_srcdir)/share
373
374#----------------------------------------------------------------------
375# Definitions for the distribution file
376#----------------------------------------------------------------------
377
378DISTRIBUTION = $(PRODUCT)-$(VERSION)
379
380# Directories to include in the distribution file
381
382DISTDIRS = src helpers share share/help obj doc examples \
383        $(addprefix examples/,$(EXAMPLES)) $(addprefix src/,$(PKGS))
384
385# Build/install helper files
386
387HELPERS = $(addprefix helpers/, \
388        install-sh mkinstalldirs config.guess config.sub dependency.make)
389
390# Files to include in the distribution file
391
392DISTFILES = \
393        README INSTALL NEWS \
394        configure configure.in Makefile.in $(HELPERS) \
395        vis.1 \
396        xsimv \
397        $(CSRC) $(HEADERS) $(LEXSRC) $(YACCSRC) $(MAKEINCLUDES) \
398        $(EXAMPLEFILES) \
399        $(addprefix doc/,$(DOCUMENTATION)) \
400        $(addprefix share/,$(SHAREFILES)) \
401        $(addprefix share/help/,$(HELPFILES))
402
403#----------------------------------------------------------------------
404# Variables used by for Revision Control
405#----------------------------------------------------------------------
406
407# The root RCS directory
408rcs_rootdir          = /projects/vis/rcsRoot/common
409
410RCSFILES        = $(CSRC) $(HEADERS) $(LEXSRC) $(YACCSRC) $(MAKEINCLUDES)
411
412RCSMISCFILES      = Makefile.in configure.in localconfigure \
413        masterconfigure README INSTALL NEWS xsimv $(addprefix helpers/, mkinstalldirs install-sh \
414                config.guess config.sub dependency.make )
415
416RCSSHAREFILES        = $(SHAREFILES)
417
418#----------------------------------------------------------------------
419# Implicit rules
420#----------------------------------------------------------------------
421
422ALLCFLAGS = $(CFLAGS) $(AC_FLAGS) $(VERDATE) \
423                -DNAWK=\"$(NAWK)\" -DLIBRARY=\"$(datadir)\"
424
425# For compiling a source file into the object directory
426
427$(objectdir)/%.o : %.c
428        umask 2 ; $(CC) -c $(ALLCFLAGS) $(INCLUDEDIRS) -o $@ $<
429
430# Place object files into an archive
431
432%.a :
433        rm -f $@
434        umask 2; $(AR) cq $@ $^
435        $(RANLIB) $@
436
437######################################################################
438#                               RULES                                #
439######################################################################
440
441#:
442#: Useful targets:
443#:
444
445#----------------------------------------------------------------------
446# Rule for getting help
447#----------------------------------------------------------------------
448
449.PHONY : help
450
451#: help -- Print a list of targets
452
453# This prints all lines in this Makefile that begin with #:
454
455help :
456        @sed -n "s/^#://p" Makefile
457
458#----------------------------------------------------------------------
459# Always executed once when the Makefile is run
460#----------------------------------------------------------------------
461
462# Make sure the directory in which to place the objects exists
463
464ignored := $(shell umask 2; test -d $(objectdir) || mkdir $(objectdir))
465
466#----------------------------------------------------------------------
467# Rules to compile and build libraries and executables
468#----------------------------------------------------------------------
469
470.PHONY : all allprods library allprods-mp exe-mp compile-version delete-version
471
472#:
473#: all (the default) -- Compile the main executable
474# (force the version to be recompiled)
475
476all : ALLCFLAGS += -DBDD$(BDDPKG)
477
478all : compile-version $(PRODUCT)
479
480# Create the main executable
481$(PRODUCT) : $(OBJECTS) $(glulibdir)/libglu.a $(glulibdir)/lib$(BDDPKG).a
482        umask 2 ; $(LINKER) -o $(PRODUCT) $(LDFLAGS) \
483                $(OBJECTS) $(LIBRARYDIRS) $(LIBS)
484
485#: allprods -- Compile an executable linked with each BDD package
486
487allprods : $(OBJECTS) $(glulibdir)/libglu.a $(foreach bddpkg, $(BDDPKGS), \
488           $(glulibdir)/lib$(bddpkg).a)
489        @for bddpkg in $(BDDPKGS) ; \
490        do \
491          rm -f $(objectdir)/satBDD.o; \
492          umask 2 ; $(CC) -c $(ALLCFLAGS) -DBDD$$bddpkg $(INCLUDEDIRS) -o $(objectdir)/satBDD.o  $(master_srcdir)/src/sat/satBDD.c; \
493          echo "Creating vis-$$bddpkg";\
494          umask 2 ; $(LINKER) -o $(PRODUCT)-$$bddpkg $(LDFLAGS) $(OBJECTS) \
495                $(LIBRARYDIRS) $(VISLIBS) -l$$bddpkg -lglu $(OTHERLIBS); \
496        done
497
498# Force the "version" information to be recompiled
499
500compile-version : delete-version $(objectdir)/vmVers.o $(objectdir)/satBDD.o
501
502# Delete the object file related to the version
503
504delete-version :
505        rm -f $(objectdir)/vmVers.o $(objectdir)/satBDD.o
506
507# Build a library containing all the objects
508
509#: library -- Create a library of all the objects (useful in a central area)
510
511library : $(LIBRARY)
512
513$(LIBRARY) : $(OBJECTS)
514
515ifdef PLINKER
516$(PRODUCT)-mp : $(LIBRARY) $(glulibdir)/libglu.a \
517                $(foreach bddpkg, $(BDDPKGS), \
518                $(glulibdir)/lib$(bddpkg).a)
519        umask 2 ; $(PLINKER) -o $(PRODUCT)-mp $(OBJECTS) \
520                `purify -printhomedir`/libpurify_stubs.a \
521                $(LIBRARYDIRS) $(LIBS)
522
523allprods-mp : $(LIBRARY) $(glulibdir)/libglu.a \
524                $(foreach bddpkg, $(BDDPKGS), \
525                $(glulibdir)/lib$(bddpkg).a)
526        @for bddpkg in $(BDDPKGS) ; \
527        do \
528          echo "Creating vis-$$bddpkg";\
529          umask 2 ; $(PLINKER) -o $(PRODUCT)-$$bddpkg-mp $(OBJECTS) \
530                `purify -printhomedir`/libpurify_stubs.a \
531                $(LIBRARYDIRS) $(VISLIBS) -l$$bddpkg -lglu $(OTHERLIBS) ; \
532        done
533
534exe-mp : $(OBJECTS)
535        $(PLINKER) -o $(PRODUCT)-mp $(OBJECTS) \
536                `purify -printhomedir`/libpurify_stubs.a \
537                $(LIBRARYDIRS) $(LIBS)
538endif
539
540#----------------------------------------------------------------------
541# Rule to produce the function map for the memory_profile command
542#----------------------------------------------------------------------
543
544.PHONY : functionmap
545
546FMAPFILE = .fmap
547functionmap: $(CSRC)
548        $(VIS)/common/share/createfunctionmap $^ >$(FMAPFILE)
549
550#----------------------------------------------------------------------
551# Rules for installation
552#----------------------------------------------------------------------
553
554.PHONY : install uninstall installdirs
555
556#:
557#: install -- Install the product and libraries in bindir, libdir,
558#:            datadir, etc.
559
560install : $(PRODUCT) $(LIBRARY) installdirs
561        @echo "Installing $(bindir)/$(PRODUCT)"
562        @$(INSTALL_PROGRAM) $(PRODUCT) $(bindir)/$(PRODUCT)
563        @echo "Installing $(libdir)/$(LIBRARY)"
564        @$(INSTALL_DATA) $(LIBRARY) $(libdir)/$(LIBRARY)
565        @for file in $(SHAREFILES) ; do \
566                echo "Installing $(datadir)/$$file"; \
567                $(INSTALL_DATA) $(master_srcdir)/share/$$file \
568                        $(datadir)/$$file; \
569        done
570        @for file in $(HELPFILES) ; do \
571                echo "Installing $(datadir)/help/$$file"; \
572                $(INSTALL_DATA) $(master_srcdir)/share/help/$$file \
573                        $(datadir)/help/$$file; \
574        done
575        @echo "Installing $(mandir)/vis.1"
576        @$(INSTALL_DATA) vis.1 $(mandir)/vis.1
577        @for header in $(HEADERS); do \
578                echo "Installing $(includedir)/$$header"; \
579                $(INSTALL_DATA) $(master_srcdir)/src/*/$$header \
580                        $(includedir)/$$header; \
581        done
582
583#: uninstall -- Reverse the effects of "install"
584
585uninstall :
586        rm -f $(bindir)/$(PRODUCT)
587        rm -f $(libdir)/$(LIBRARY)
588        @for file in $(SHAREFILES) ; \
589        do \
590          echo "Removing $(datadir)/$$file"; \
591          rm -f $(datadir)/$$file; \
592        done
593        @for file in $(HELPFILES) ; \
594        do \
595          echo "Removing $(datadir)/help/$$file"; \
596          rm -f $(datadir)/help/$$file; \
597        done
598        @for header in $(HEADERS); \
599        do \
600          echo "Removing $(includedir)/$$header"; \
601          rm -f $(includedir)/$$header; \
602        done
603
604installdirs :
605        $(master_srcdir)/helpers/mkinstalldirs \
606                $(bindir) $(libdir) $(includedir) $(datadir) $(datadir)/help \
607                $(mandir)
608
609#----------------------------------------------------------------------
610# Rules for checking the build
611#----------------------------------------------------------------------
612
613.PHONY : check check-examples
614
615# This is a lengthy sed command used to filter out the irrelevant VIS
616# output that appears when the examples are running.
617#
618# Sed does not permit space between the trailing p ("print matching
619# lines") and the semicolon (end of command).  Hashes are escaped --
620# otherwise they are Makefile comments.  This was once a long egrep
621# expression, but the string was too long for Ultrix's egrep.
622
623SED_CMD = \
624        /^FSM depth/p; \
625        /^computation depth/p; \
626        /^reachable states =/p; \
627        /^\# MC: formula passed/p; \
628        /^\# MC: formula failed/p; \
629        /^\# MC: the number of non-trivial forced segments/p; \
630        /^\# MC: Vacuous/p; \
631        /^\# MC: No vacuous/p; \
632        /[sS]tates covered/p; \
633        /covered states/p; \
634        /Percentage of coverage/p; \
635        /^\# LTL_MC: formula passed/p; \
636        /^\# LTL_MC: formula failed/p; \
637        /^\# INV: formula passed/p; \
638        /^\# INV: formula failed/p; \
639        /^\# LE: language is not empty/p; \
640        /^\# LE: language emptiness check passes/p; \
641        /^\# ABS: formula passed/p; \
642        /^\# ABS: formula failed/p; \
643        /^\# BMC: formula failed/p;\
644        /^\# BMC: no counterexample found/p; \
645        /Residue/p; \
646        /^\# AMC: Verified formula TRUE/p; \
647        /^\# AMC: Verified formula FALSE/p; \
648        /Equivalence Classes/p; \
649        /Total number of literals/p; \
650        /Networks are combinationally equivalent\./p; \
651        /Networks are sequentially equivalent\./p; \
652        /;.*;/p;
653
654CHECK_EXAMPLES_cu = daio_receiver mult6x6 s1269 fpmpy restruct synthesis \
655        production_cell
656CHECK_EXAMPLES_cmu =
657CHECK_EXAMPLES_cal =
658
659# List of all examples to check (A subset of EXAMPLES)
660
661CHECK_COMMON_EXAMPLES = abp amp arbiter bakery coherence counter crd ctlp3 \
662        dcnew eisenberg elevator ethernet exampleS gcd gigamax ping_pong \
663        scheduler short slider tbl_one_bug tcp tlc treearbiter
664
665CHECK_EXAMPLES = $(CHECK_COMMON_EXAMPLES) $(CHECK_EXAMPLES_$(BDDPKG))
666
667# Determine the absolute executable path
668#
669# Starting from the current directory, change directory to the directory
670# part of the product name, then tack on the filename part of EXECUTABLE
671
672EXECUTABLE = $(PRODUCT)
673
674EXECUTABLEPATH := \
675        $(shell cd $(dir $(EXECUTABLE)) ; pwd)/$(notdir $(EXECUTABLE))
676
677# Determine the rootname of the examples
678#
679
680EXAMPLEPATH = $(master_srcdir)/examples
681
682FULLEXAMPLEPATH := $(shell cd $(EXAMPLEPATH) ; pwd)
683
684#:
685#: check -- Test the locally-built executable (runs check-examples)
686
687check : check-examples
688
689# Run check on each of the bdd versions (named e.g., vis-cmu)
690
691#: check-allprods -- Test each of the BDD executables (see allprods)
692
693check-allprods :
694        @for bddpkg in $(BDDPKGS) ; \
695        do \
696          echo "Checking $(PRODUCT)-$$bddpkg";\
697          $(MAKE) PRODUCT=$(PRODUCT)-$$bddpkg BDDPKG=$$bddpkg check ; \
698        done
699
700#: check-examples -- Test each of the examples listed in CHECK_EXAMPLES
701#:          You may want to invoke this with
702#:            gmake "CHECK_EXAMPLES=abp bakery" check-examples
703#:            gmake EXECUTABLE=vis-cmu check-examples
704#:            gmake EXECUTABLE=/projects/vis/vis-devel/alpha-g/vis \
705#:                    check-examples
706#:            gmake EXAMPLEPATH=/projects/vis/vis-devel/common/examples \
707#:                    check-examples
708#:            gmake EXAMPLEPATH=../common/examples check-examples
709#:            gmake VIS_LIBRARY_PATH=/projects/vis/vis-devel/share
710
711# For each example,
712#
713# 1) create the directory checkresults/<example>
714# 2) enter that directory
715# 3) create "check_script" by prepending a "set open_path" command
716#    to the example's check_script in the master source directory.  This
717#    makes VIS look in the master source directory for example files
718# 4) run VIS on that script, producing "result.raw"
719# 5) filter out relevant lines in the result, producing "result.filtered"
720#    and compare this with the "check_result" file in the master source
721#    directory.  Differences are written to "result.differences"
722
723check-examples :
724        @test -d checkresults || mkdir checkresults
725        @echo "Checking examples.  Results will be in checkresults/<example>/result.raw"
726        @echo "Running executable $(EXECUTABLEPATH)"
727        @echo " (change with EXECUTABLE=...)"
728        @echo "Taking examples from $(FULLEXAMPLEPATH)"
729        @echo " (change with EXAMPLEPATH=...)"
730        @cwd=`pwd` ; \
731        VIS_LIBRARY_PATH=$(VIS_LIBRARY_PATH) ; \
732        export VIS_LIBRARY_PATH ; \
733        for example in $(CHECK_EXAMPLES) ; \
734        do \
735          echo -n "Checking $$example ... " ; \
736          cd $$cwd ; \
737          test -d checkresults/$$example || \
738                mkdir checkresults/$$example ; \
739          cd checkresults/$$example ; \
740          rm -f check_script ; \
741          echo "set open_path $(FULLEXAMPLEPATH)/$$example" > check_script ; \
742          cat $(FULLEXAMPLEPATH)/$$example/check_script >> check_script ; \
743          $(EXECUTABLEPATH) -f check_script -x > result.raw 2> result.stderr ; \
744          sed -n '$(SED_CMD)' result.raw > result.filtered ; \
745          if diff result.filtered \
746                $(FULLEXAMPLEPATH)/$$example/check_result > result.differences ; \
747          then \
748            echo "passed" ; \
749            rm result.differences ; \
750          else \
751            echo "failed (more checkresults/$$example/result.differences)" ; \
752          fi ; \
753        done
754
755#         egrep '$(KEY_WORDS)' result.raw > result.filtered ; \
756
757#----------------------------------------------------------------------
758# Rules that produce/delete the dependency file for every package
759#----------------------------------------------------------------------
760
761.PHONY : dependencies cleandependencies
762
763#:
764#: dependencies -- Create a list of dependency files.
765#:                 Useful when modifying header files.
766
767# Invoke the "dependency.make" Makefile on each package subdirectory,
768# passing the path, etc. to it.
769#
770# There's a strange feature in autoconf where lines of the form " VPATH="
771# are removed from the Makefile.  Thus, a flag is placed before the
772# VPATH= argument below.
773
774dependencies:
775ifneq ($(findstring <$(CC)>,<gcc> <g++> <icc> <icpc>),)
776        for pkg in $(PKGS) ; \
777        do \
778          $(MAKE) --no-print-directory \
779                -f $(master_srcdir)/helpers/dependency.make \
780                CC="$(CC)" \
781                CFLAGS="$(CFLAGS)" VPATH="$(local_srcdir)/src/$$pkg" \
782                AC_FLAGS="$(AC_FLAGS)" \
783                INCLUDEDIRS="$(INCLUDEDIRS)" objectdir=$(objectdir) \
784                PKGNAME=$(local_srcdir)/src/$$pkg/$$pkg \
785                $(local_srcdir)/src/$$pkg/$$pkg.d ; \
786        done
787else
788        @echo "dependency requires gcc, g++, icc, or icpc"
789        @echo "Reconfigure with gcc, g++, icc, or icpc"
790endif
791
792cleandependencies:
793        rm -f $(local_srcdir)/src/*/*.d
794
795#----------------------------------------------------------------------
796# Rules for making a distribution file
797#----------------------------------------------------------------------
798
799.PHONY : dist
800
801#:
802#: dist -- Create a tarred, gzipped distribution file
803
804# Warning: "tar" under Digital Unix (on DEC Alphas) writes directories
805# that don't work under SunOS tar
806
807dist : $(DISTRIBUTION).tar.gz
808
809$(DISTRIBUTION).tar.gz : $(DISTFILES)
810ifeq ($(strip $(FULL_MISSING_PKGS)),)
811        rm -rf $(DISTRIBUTION)
812        umask 022; mkdir $(DISTRIBUTION)
813        for dir in $(DISTDIRS); \
814        do \
815          umask 022; mkdir $(DISTRIBUTION)/$$dir; \
816        done
817        @echo "Copying distribution files"
818        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
819        do \
820          echo "  $$file"; \
821          cp -p $(local_srcdir)/$$file $(DISTRIBUTION)/$$file; \
822        done
823        - chmod -R a+r $(DISTRIBUTION)
824        - chmod -R u+w $(DISTRIBUTION)
825        tar cf - $(DISTRIBUTION) | gzip -9 > $(DISTRIBUTION).tar.gz
826        rm -rf $(DISTRIBUTION)
827else
828        @echo "Missing packages: $(FULL_MISSING_PKGS)"
829        @echo "Make sure PKGS lists all the packages"
830        @exit 1
831endif
832
833#----------------------------------------------------------------------
834# Rules for rebuilding the configure file and Makefile
835#----------------------------------------------------------------------
836
837${master_srcdir}/configure : configure.in
838        cd ${master_srcdir} && autoconf
839        chmod 0775 ${master_srcdir}/config*
840
841config.status : configure
842        ./config.status --recheck
843
844Makefile : Makefile.in config.status
845        @echo "The master Makefile.in has been changed:"
846        @echo "run config.status"
847        @echo "Warning: This will overwrite any local Makefile modifications"
848        @exit 1
849
850#----------------------------------------------------------------------
851# Rules for cleaning
852#----------------------------------------------------------------------
853
854.PHONY : clean mostlyclean distclean
855
856#:
857#: clean -- Remove every file created by building
858
859clean mostlyclean :
860        rm -rf $(objectdir)/* $(LIBRARY) $(PRODUCT) \
861                $(foreach bddpkg, $(BDDPKGS), $(PRODUCT)-$(bddpkg)) \
862                checkresults include
863
864#: distclean -- Remove every file created by building or configuring
865
866distclean : clean cleandependencies
867        rm -f Makefile config.status config.cache config.log
868
869#----------------------------------------------------------------------
870# Rule for performing a lint-like check on the source code
871#
872# Note: This requires gcc or g++
873#----------------------------------------------------------------------
874
875.PHONY : check-code
876
877#:
878#: check-code -- Run a lint-like check on the source code.
879#:               (useful for development)
880
881CHECK_FLAGS := -Wall -pedantic -DBDD$(BDDPKG)
882ifeq ($(CC),gcc)
883  CHECK_FLAGS += -Wstrict-prototypes -Wmissing-prototypes -Wmissing-declarations
884endif
885
886check-code : $(CSRC) $(BDD_CSRC) $(MDD_CSRC)
887ifneq ($(findstring <$(CC)>,<gcc> <g++>),)
888        @rm -f *.o_checkcode
889        @for file in $^; \
890        do \
891          echo "------------------------ Checking $$file"; \
892          $(CC) -c $(CFLAGS) $(AC_FLAGS) $(CHECK_FLAGS) \
893                $(VERDATE) $(INCLUDEDIRS) \
894                -o $(objectdir)/checkcode_output.o $$file; \
895          rm -f $(objectdir)/checkcode_output.o; \
896        done
897        @rm -f *.o_checkcode
898else
899        @echo "check-code requires gcc or g++"
900        @echo "Reconfigure with gcc or g++"
901endif
902
903#----------------------------------------------------------------------
904# Rule for generating function prototypes for all the
905# source and header files in all the PKGS
906#
907# Note: This requires "extproto," part of the ext package available from
908# ftp://ic.eecs.berkeley.edu/pub/Ext
909#----------------------------------------------------------------------
910
911.PHONY : proto
912
913#:
914#: proto -- Regenerate all the function prototypes in the packages
915#:          Useful during development.  You may want to invoke it with
916#:            gmake "PKGS=tst tbl" proto
917
918proto :
919        @cd $(local_srcdir)/src ; \
920        for pkg in $(PKGS); \
921        do \
922          cd $$pkg ; \
923          extproto *.h *.c ; \
924          cd .. ; \
925        done
926
927#----------------------------------------------------------------------
928# Rules for generating the documentation and command help files
929# for all the packages
930#
931# Note: This requires "extdoc," part of the ext package, and
932# lynx, a textual WWW browser
933#----------------------------------------------------------------------
934
935.PHONY : allDoc doc indices helpfiles cleandoc
936
937#:
938#: allDoc -- Extract all the documentation (runs doc, indices, and helpfiles)
939
940allDoc : cleandoc doc indices helpfiles
941
942#: doc -- Extract HTML and text documentation on all the functions
943
944doc : $(htmldocdir) $(txtdocdir)
945        for pkg in $(PKGS); \
946        do \
947          umask 2 ; extdoc --html=$(htmldocdir) --text=$(txtdocdir) \
948                $(local_srcdir)/src/$$pkg/$$pkg; \
949        done
950
951#: indices -- Generate function and command indices for the HTML documentation
952
953indices : $(htmldocdir)
954        umask 2 ; extindex $(htmldocdir)
955
956#: helpfiles -- Generate the help files from the HTML documentation
957
958helpfiles : $(helpdir)
959        for file in $(htmldocdir)/*Cmd.html ; \
960        do \
961          echo Converting $$file ; \
962          umask 2 ; lynx -dump $$file > $(helpdir)/`basename $$file .html`.txt ; \
963        done
964
965#: cleandoc -- Remove all the documentation generated by "allDoc"
966
967cleandoc :
968        -rm -f $(htmldocdir)/*.html
969        -rm -f $(txtdocdir)/*.txt
970        -rm -f $(helpdir)/*Cmd.txt
971
972$(htmldocdir) :
973        - umask 2 ; mkdir $(htmldocdir)
974
975$(txtdocdir) :
976        - umask 2 ; mkdir $(txtdocdir)
977
978$(helpdir) :
979        - umask 2 ; mkdir $(helpdir)
980
981
982#----------------------------------------------------------------------
983# Revision control rules
984#
985# May be invoked with command-line overrides, e.g.,
986# gmake RCSFILES=foo.c rcs_co
987# gmake PKGS=array rcs_ci
988#----------------------------------------------------------------------
989
990.PHONY: rcs_ci rcs_co rcs_diff rcs_ident rcs_status
991
992#:
993#:       You may want to invoke the RCS rules with
994#:         gmake "PKGS=tst tbl" rcs_ci
995#:         gmake "RCSFILES=tstMain.c" rcs_co
996#:
997#: rcs_ci -- check in user-modified files and put an updated copy
998#:           in the central area
999
1000rcs_ci: $(RCSFILES)
1001        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1002        do \
1003          ci -u $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1004          co -u $(RCSFLAGS) $(master_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1005        done
1006
1007#: rcs_co -- check out files for modification
1008
1009rcs_co: $(RCSFILES)
1010        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1011        do \
1012          co -l $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1013        done
1014
1015#: rcs_diff -- Report differences between local files and checked-in versions
1016
1017rcs_diff: $(RCSFILES)
1018        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1019        do \
1020          rcsdiff $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1021        done
1022
1023#: rcs_ident -- Print the RCS identifier in each file
1024
1025rcs_ident: $(RCSFILES)
1026        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1027        do \
1028          ident $(RCSFLAGS) $(local_srcdir)/$$file; \
1029        done
1030
1031#: rcs_status -- Report who has checked out files
1032
1033rcs_status: $(RCSFILES)
1034        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1035        do \
1036          rlog -L -h $(RCSFLAGS) $(rcs_rootdir)/$$file,v; \
1037        done
1038
1039#----------------------------------------------------------------------
1040# RCS rules for common/{Makefile.in, configure.in, localconfigure,
1041# masterconfigure, mkinstalldirs, install-sh}
1042#----------------------------------------------------------------------
1043
1044.PHONY : rcs_ci_misc rcs_co_misc rcs_diff_misc
1045
1046#: rcs_ci_misc -- Check in miscellaneous files, updating central area
1047
1048rcs_ci_misc: $(RCSMISCFILES)
1049        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1050        do \
1051          ci -u $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1052          co -u $(RCSFLAGS) $(master_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1053        done
1054
1055#: rcs_co_misc -- Check out miscellaneous files
1056
1057rcs_co_misc: $(RCSMISCFILES)
1058        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1059        do \
1060          co -l $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1061        done
1062
1063#: rcs_diff_misc -- Report differences in miscellaneous files
1064
1065rcs_diff_misc: $(RCSMISCFILES)
1066        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1067        do \
1068          rcsdiff $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1069        done
1070
1071#: rcs_ident_misc -- Report RCS identifiers
1072
1073rcs_ident_misc: $(RCSMISCFILES)
1074        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1075        do \
1076          ident $(RCSFLAGS) $(local_srcdir)/$$file; \
1077        done
1078
1079#: rcs_status_misc -- Report checked in/out status, ownership
1080
1081rcs_status_misc: $(RCSMISCFILES)
1082        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1083        do \
1084          rlog -L -h $(RCSFLAGS) $(rcs_rootdir)/$$file,v; \
1085        done
1086
1087#----------------------------------------------------------------------
1088# RCS rules for files in common/share
1089#----------------------------------------------------------------------
1090
1091.PHONY : rcs_ci_share rcs_co_share rcs_diff_share
1092
1093#: rcs_ci_share -- Check in files in the share/ directory
1094
1095rcs_ci_share: $(RCSSHAREFILES)
1096        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1097        do \
1098          ci -u $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1099          co -u $(RCSFLAGS) $(master_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1100        done
1101
1102#: rcs_co_share -- Check out share files
1103
1104rcs_co_share: $(RCSSHAREFILES)
1105        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1106        do \
1107          co -l $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1108        done
1109
1110#: rcs_diff_share -- Report differences in share files
1111
1112rcs_diff_share: $(RCSSHAREFILES)
1113        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1114        do \
1115          rcsdiff $(RCSFLAGS) $(local_srcdir)/$$file $(rcs_rootdir)/$$file,v; \
1116        done
1117
1118#: rcs_ident_share -- Report RCS identifiers
1119
1120rcs_ident_share: $(RCSSHAREFILES)
1121        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1122        do \
1123          ident $(RCSFLAGS) $(local_srcdir)/$$file; \
1124        done
1125
1126#: rcs_status_share -- Report checked in/out status, ownership
1127
1128rcs_status_share: $(RCSSHAREFILES)
1129        @for file in $(patsubst $(local_srcdir)/%, %, $^); \
1130        do \
1131          rlog -L -h $(RCSFLAGS) $(rcs_rootdir)/$$file,v; \
1132        done
1133
1134#----------------------------------------------------------------------
1135# Rules for debugging the Makefile
1136#----------------------------------------------------------------------
1137
1138.PHONY : debug-make
1139
1140DEBUG_VARS =    ALL_PKGS \
1141                PKGS \
1142                MISSING_PKGS \
1143                VPATH \
1144                INCLUDEDIRS \
1145                CSRC \
1146                OBJECTS \
1147                HEADERS \
1148                MAKEINCLUDES \
1149                CFLAGS \
1150                AC_FLAGS \
1151                master_srcdir \
1152                local_srcdir \
1153                RCSFILES \
1154                RCSDIR \
1155                LIBS \
1156                VISLIBS \
1157                DISTFILES \
1158                EXAMPLEFILES
1159
1160#:
1161#: debug-make -- Print a list of Makefile variables
1162
1163debug-make:
1164        @$(foreach var, $(DEBUG_VARS), echo $(var)=$($(var)) ; )
Note: See TracBrowser for help on using the repository browser.