Context Navigation

Makefile.in @ 101

Last change on this file since 101 was 28, checked in by cecile, 13 years ago
exemples de test
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
47	default : 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
55	PKGS = $(ALL_PKGS)
56
57	# The name of the BDD package to use
58
59	BDDPKG = @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
96	ALL_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 debug var vm
99	# Generate the list of all packages NOT in the PKGS list
100
101	MISSING_PKGS = $(filter-out $(PKGS), $(ALL_PKGS))
102
103	# All the BDD packages
104	BDDPKGS = cu cmu cal
105
106	#----------------------------------------------------------------------
107	# For safety
108	#----------------------------------------------------------------------
109
110	SHELL = /bin/sh
111	.SUFFIXES:
112
113	#----------------------------------------------------------------------
114	# The name of the product and its version
115	#----------------------------------------------------------------------
116
117	PRODUCT = vis
118	VERSION = 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
125	VERDATE := -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=
134	master_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=
140	local_srcdir = @local_srcdir@
141
142	#----------------------------------------------------------------------
143	# Directories used while building
144	#----------------------------------------------------------------------
145
146	# Directories to search for glu .h files (space-separated)
147	gluincdir1 = @gluincdir@
148
149	# Directories to search for libglu.a (space-separated)
150	glulibdir1 = @glulibdir@
151
152	# Directory where object files will be placed during the build
153	objectdir = obj
154
155	# Directory where links to header files will be placed during the build
156	headerdir = $(local_srcdir)/include
157
158	# Directories where documentation will be placed during the build
159	docdir = $(master_srcdir)/doc
160	htmldocdir = $(docdir)/html
161	txtdocdir = $(docdir)/txt
162	helpdir = $(master_srcdir)/share/help
163
164	# Directories to search for VIS library files
165	# Set by ./configure --with-vis-libdir=
166	vislibdir = @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
174	VIS_LIBRARY_PATH = $(shell cd $(master_srcdir)/share ; pwd)
175
176	#----------------------------------------------------------------------
177	# Defaults for GLU library and header files
178	#----------------------------------------------------------------------
179
180	ifndef gluincdir1
181	gluincdir = ../glu-$(VERSION)/include ../../glu-$(VERSION)/include
182	else
183	gluincdir = $(gluincdir1) $(gluincdir1)/../src/cudd
184	endif
185
186	ifndef glulibdir1
187	glulibdir = ../glu-$(VERSION) ../../glu-$(VERSION)
188	else
189	glulibdir = $(glulibdir1)
190	endif
191
192	#----------------------------------------------------------------------
193	# Installation names and directories
194	#----------------------------------------------------------------------
195
196	# Name of the library to create
197	LIBRARY = lib$(PRODUCT).a
198
199	# Name of the man page
200	MANPAGE = vis.1
201
202	# Directory in which to install architecture-independent files
203	# Set by ./configure --prefix=...
204	prefix = @prefix@
205
206	# Directory in which to install architecture-dependent files
207	# Set by ./configure --exec-prefix=...
208	exec_prefix = @exec_prefix@
209
210	# Directory in which to install binaries
211	bindir = $(exec_prefix)/bin
212
213	# Directory in which to install libraries
214	libdir = $(exec_prefix)/lib
215
216	# Directory in which to install headers
217	includedir = $(prefix)/include
218
219	# Directory in which to install architecture-independent library files
220	datadir = $(prefix)/share/vis
221
222	# Directory for the man page
223	mandir = $(prefix)/man/man1
224
225	#----------------------------------------------------------------------
226	# The following are set by the configure script
227	#----------------------------------------------------------------------
228
229	AC_FLAGS = @DEFS@
230	LIBDIRS = @LIBDIRS@
231	RANLIB = @RANLIB@
232	CC = @CC@
233	LINKER = @LINKER@
234	LDFLAGS = @LDFLAGS@
235	#
236	# Define the linker for the executable with "memory_profile" activated
237	#
238	PLINKER = @PLINKER@
239	CFLAGS = @CFLAGS@
240	OTHERLIBS = -lm @LIBS@ @LEXLIB@
241	YACC = @YACC@
242	LEX = @LEX@
243	NAWK = @AWK@
244	INSTALL = @INSTALL@
245	INSTALL_PROGRAM = @INSTALL_PROGRAM@
246	INSTALL_DATA = @INSTALL_DATA@
247	AR = @AR@
248	ZCHAFF= @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
258	EXAMPLES = $(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
268	EXAMPLEFILES = $(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
280	DOCUMENTATION = blifmv.ps ctl.ps vis_user.ps two_phase.ps
281
282	#----------------------------------------------------------------------
283	# Files in the share directory
284	#----------------------------------------------------------------------
285
286	SHAREFILES = 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
294	HELPFILES = $(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
309	MAKEINCLUDES = $(foreach package, $(PKGS), \
310	$(local_srcdir)/src/$(package)/$(package).make)
311
312	include $(MAKEINCLUDES)
313
314	OBJECTS = $(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
321	DEPENDENCIES = $(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
334	INCLUDEDIRS = $(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
340	LIBRARYDIRS = $(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
346	ifneq ($(strip $(MISSING_PKGS)),)
347	VISLIBS = -l$(PRODUCT)
348	else
349	VISLIBS =
350	endif
351
352	GLULIBS = -l$(BDDPKG) -lglu
353
354	# g++ on Linux RH requires -lstdc++
355	ifeq ($(CC),g++)
356	OTHERLIBS += -lstdc++
357	endif
358
359	LIBS = $(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
367	VPATH = $(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
378	DISTRIBUTION = $(PRODUCT)-$(VERSION)
379
380	# Directories to include in the distribution file
381
382	DISTDIRS = src helpers share share/help obj doc examples \
383	$(addprefix examples/,$(EXAMPLES)) $(addprefix src/,$(PKGS))
384
385	# Build/install helper files
386
387	HELPERS = $(addprefix helpers/, \
388	install-sh mkinstalldirs config.guess config.sub dependency.make)
389
390	# Files to include in the distribution file
391
392	DISTFILES = \
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
408	rcs_rootdir = /projects/vis/rcsRoot/common
409
410	RCSFILES = $(CSRC) $(HEADERS) $(LEXSRC) $(YACCSRC) $(MAKEINCLUDES)
411
412	RCSMISCFILES = Makefile.in configure.in localconfigure \
413	masterconfigure README INSTALL NEWS xsimv $(addprefix helpers/, mkinstalldirs install-sh \
414	config.guess config.sub dependency.make )
415
416	RCSSHAREFILES = $(SHAREFILES)
417
418	#----------------------------------------------------------------------
419	# Implicit rules
420	#----------------------------------------------------------------------
421
422	ALLCFLAGS = $(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
455	help :
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
464	ignored := $(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
476	all : ALLCFLAGS += -DBDD$(BDDPKG)
477
478	all : 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
487	allprods : $(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
500	compile-version : delete-version $(objectdir)/vmVers.o $(objectdir)/satBDD.o
501
502	# Delete the object file related to the version
503
504	delete-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
511	library : $(LIBRARY)
512
513	$(LIBRARY) : $(OBJECTS)
514
515	ifdef 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
523	allprods-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
534	exe-mp : $(OBJECTS)
535	$(PLINKER) -o $(PRODUCT)-mp $(OBJECTS) \
536	`purify -printhomedir`/libpurify_stubs.a \
537	$(LIBRARYDIRS) $(LIBS)
538	endif
539
540	#----------------------------------------------------------------------
541	# Rule to produce the function map for the memory_profile command
542	#----------------------------------------------------------------------
543
544	.PHONY : functionmap
545
546	FMAPFILE = .fmap
547	functionmap: $(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
560	install : $(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
585	uninstall :
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
604	installdirs :
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
623	SED_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
654	CHECK_EXAMPLES_cu = daio_receiver mult6x6 s1269 fpmpy restruct synthesis \
655	production_cell
656	CHECK_EXAMPLES_cmu =
657	CHECK_EXAMPLES_cal =
658
659	# List of all examples to check (A subset of EXAMPLES)
660
661	CHECK_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
665	CHECK_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
672	EXECUTABLE = $(PRODUCT)
673
674	EXECUTABLEPATH := \
675	$(shell cd $(dir $(EXECUTABLE)) ; pwd)/$(notdir $(EXECUTABLE))
676
677	# Determine the rootname of the examples
678	#
679
680	EXAMPLEPATH = $(master_srcdir)/examples
681
682	FULLEXAMPLEPATH := $(shell cd $(EXAMPLEPATH) ; pwd)
683
684	#:
685	#: check -- Test the locally-built executable (runs check-examples)
686
687	check : 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
693	check-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
723	check-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
774	dependencies:
775	ifneq ($(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
787	else
788	@echo "dependency requires gcc, g++, icc, or icpc"
789	@echo "Reconfigure with gcc, g++, icc, or icpc"
790	endif
791
792	cleandependencies:
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
807	dist : $(DISTRIBUTION).tar.gz
808
809	$(DISTRIBUTION).tar.gz : $(DISTFILES)
810	ifeq ($(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)
827	else
828	@echo "Missing packages: $(FULL_MISSING_PKGS)"
829	@echo "Make sure PKGS lists all the packages"
830	@exit 1
831	endif
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
841	config.status : configure
842	./config.status --recheck
843
844	Makefile : 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
859	clean 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
866	distclean : 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
881	CHECK_FLAGS := -Wall -pedantic -DBDD$(BDDPKG)
882	ifeq ($(CC),gcc)
883	CHECK_FLAGS += -Wstrict-prototypes -Wmissing-prototypes -Wmissing-declarations
884	endif
885
886	check-code : $(CSRC) $(BDD_CSRC) $(MDD_CSRC)
887	ifneq ($(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
898	else
899	@echo "check-code requires gcc or g++"
900	@echo "Reconfigure with gcc or g++"
901	endif
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
918	proto :
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
940	allDoc : cleandoc doc indices helpfiles
941
942	#: doc -- Extract HTML and text documentation on all the functions
943
944	doc : $(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
953	indices : $(htmldocdir)
954	umask 2 ; extindex $(htmldocdir)
955
956	#: helpfiles -- Generate the help files from the HTML documentation
957
958	helpfiles : $(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
967	cleandoc :
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
1000	rcs_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
1009	rcs_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
1017	rcs_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
1025	rcs_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
1033	rcs_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
1048	rcs_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
1057	rcs_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
1065	rcs_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
1073	rcs_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
1081	rcs_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
1095	rcs_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
1104	rcs_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
1112	rcs_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
1120	rcs_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
1128	rcs_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
1140	DEBUG_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
1163	debug-make:
1164	@$(foreach var, $(DEBUG_VARS), echo $(var)=$($(var)) ; )

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format