|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
CADP 97b works fine on Sparc stations running Solaris 5.4, 5.5, and 5.6. However, when trying to use it on Solaris 7 as well, the following problem occurs.
The "hostinfo" command (used to create license files) core dumps on Solaris 7. This problem only occurs when one tries to install CADP 97b "Liege" on a new Solaris 7 machine. It does not occur when upgrading to Solaris 7 a machine on which CADP is already running.
The recommended solution is to upgrade to the current beta-version of CADP 99 "Ottawa", which contains a new version of "hostinfo".
Alternately, we can send to you a new version of "hostinfo" that you install to replace the file "$CADP/bin.sun5/hostinfo" shipped with CADP 97-b "Liège".
CADP 97b works fine on Sparc stations running Solaris 5.4, 5.5, and 5.6. However, when trying to use it on Solaris 7 as well, the following problem occurs.
When executing or verifying LOTOS programs, several tools (CAESAR, Exhibitor, Xsimulator...) abort with the following error message:
STACK_GROWS_DOWN is defd, but stack appears to grow up
sp = 0xffbee14c, GC_stackbottom = 0x0
stack direction 3
Abort
The problem is not in the CADP tools themselves, but in the Boehm-Demers garbage collection library (version 4.10) shipped within CADP. SOLUTION:
All the beta-versions of CADP 99 issued between July 1999 and the beginning of March 2000 have a problem with garbage collection.
Due to a mistake in setting compiler options, the garbage collector was not interfaced properly with the other tools: even if the "-gc" option was given to CAESAR and "caesar.open", garbage collection would not occur. This error was silent: the tools functioned normally, except that garbage collector was never activated, potentially leading to excessive memory consumption.
This problem was discovered when porting the garbage collection library to Windows. Correct versions of the library have been put in the CADP distribution. For various reasons, it was also necessary to change the interface conventions used by CAESAR and CAESAR.ADT to activate garbage collection. This required to modify the C code generated by CAESAR.ADT.
If you are using a version of CADP between beta-version 99-a to 99-f included, it is strongly advised to upgrade to 99-g (or higher).
If you have ``.h'' files generated by a previous version of CADP, it is recommended to remove them and generate them again. You can recognize ``.h'' files generated by the new version CAESAR.ADT as they check a macro-definition named CAESAR_ADT_GARBAGE_COLLECTION and invoke function GC_malloc(). Obsolete ``.h'' files do not contain these two identifiers.
CADP 97b works fine under ReadHat 4.* systems. However, when trying to use it on more recent versions of Linux (RedHat 5.*, RedHat 6.*, Debian 2.*), the following problem occurs.
Many tools abort with error nessages such as:
xsimulator.o(.text+0x591): undefined reference to `__setjmp'
tclCmdAH.o(.text+0xe08): undefined reference to `_xstat'
tclCmdAH.o(.text+0xf04): undefined reference to `_lxstat'
tclUnixFCmd.o(.text+0x162): undefined reference to `_xmknod'
bcg_file_1.o(.text+0x94f): undefined reference to `_xstat'
bcg_stream.o(.text+0x26b): undefined reference to `_fxstat'
...
collect2: ld returned 1 exit status
SOLUTION:
This problem is caused by an incompatible change in the C library (libc) between different versions of Linux.
The CADP executables of CADP 97b were compiled on a Linux Redhat 4.2 machine with libc version 5 (called libc5 or glibc1).
Newer Linux distributions such as RedHat 5.* or 6.* and Debian 2.0 use an incompatible C library as their default C library. This new version of the C library is version 6 (called libc6 or glibc2). For technical information about the new library glibc2, see
Notice that, even if you are still under RedHat 4.*, your C library can be glibc6 if you have upgradeed your C compiler, e.g., to egcs-1.1.1.
Starting from beta-version 99-g included, the Linux binaries included in CADP are compiled for glibc2. This implies that older versions of Linux based on libc5 will no longer be supported (this migration was decided after a technical enquiry conducted amongst all the users of CADP).
If you are still using CADP 97b "Liège" and do not want to upgrade until a stable version of CADP 99 "Ottawa" is released, the problem is to make CADP 97b work on recent Linux systems. The following explanations should help.
If you are using Debian Linux (2.1 "slink", i386):
Debian provides the packages so that one can both execute and compile old libc5 binaries. Check if you have the libc5 runtime and development libraries on your system. This can be done by typing:
dpkg -l libc5 dpkg -l libc5-altdev dpkg -l altgccIf not, install them (dpkg, apt, dselect...). For instance,
Then, set your environment variable $CADP_CC to point to the old gcc executable /usr/i486-linuxlibc1/bin/gcc to have access to old libraries and header files (for explanations about $CADP_CC, see the $CADP/INSTALLATION_2 file).
See also Sections 4.5 and 4.6 in http://www.debian.org/doc/FAQ/debian-faq-4.html.
If you are using RedHat Linux:
/usr/i486-linux-libc5/lib
For instance, at INRIA/VASY we have installed the following packages
found on the RedHat 6.1 CD-ROM:
libc-5.3.12-31
compat-binutils-5.2-2.9.1.0.23.1
compat-egcs-5.2-1.0.3a.1
compat-glibc-5.2-2.0.7.1
compat-libs-5.2-2
The problem is to compile, on a recent Linux system, a C program and to generate a executable program linked to libc5 libraries. Unfortunately, the RedHat 6.* distribution has no development package to create new libc5 executables. They only have run-time compatibility packages to run already existing libc5 executables.
Note: it seems that two packages are available for this purpose
Instead, we use for this problem the "gcc5" package provided by George B. Moody (MIT). The following steps should be applied:
More precisely, you have to download the file named "gcc5-1.0-1.i386.rpm" and install it (type "rpm -i gcc5-1.0-1.i386.rpm"). Installing this package is safe, in the sense that it will not overwrite existing system files.
warning: libdl.so.1, needed by /common/Cadp/tcl-tk/bin.iX86/libtk8.2.so, may conflict with libdl.so.2 warning: libc.so.6, needed by /usr/lib/libdl.so, may conflict with libc.so.5 warning: libc.so.6, needed by /usr/X11R6/lib/libX11.so, may conflict with libc.so.5and Xsimulator does not launch itself (there is a core dump instead).
Reason: The linker 'ld' uses libdl.so.2 instead of libdl.so.1. It seems that libdl.so.2 is recent and did not existed in previous Linux versions for which the gcc5 package has been designed.
Reason: same as Problem A.
gcc: file path prefix /usr/lib/gcc-lib/i486-linux-libc5/2.7.2.1/egcs-2.91.66/' never usedwhich is troublesome for the user and causes bcg_edit to abort.
Reason: Recently, gcc has been renamed into egcs. It seems that the gcc5 package by George B. Moody has been designed according to GCC conventions, whereas RedHat 6.1 uses now EGCS instead of GCC. By the way, the next version of bcg_edit will be made more robust, so as to resist to such unexpected compiler warnings.
# the following lines mirror libdl.so.1* in the LIBC5 package
cd /usr/i486-linux-libc5/lib/
ln -s /lib/libdl.so.1.* .
ln -s libdl.so.1.* libdl.so.1
ln -s libdl.so.1 libdl.so
# the following lines hack the GCC5 package to make it EGCS-like
cd /usr/lib/gcc-lib/i486-linux-libc5
ln -s 2.7.2.1 egcs-2.91.66
cd 2.7.2.1
ln -s /usr/i486-linux-libc5/lib/*.o .
# then edit /usr/bin/gcc5
# remove the line "export GCC_EXEC_PREFIX=/usr/i486-linux-libc5/lib//"
# replace the contents of the file with
#!/bin/bash
gcc -b i486-linux-libc5 \
-I/usr/i486-linux-libc5/include \
-I/usr/lib/gcc-lib/i486-linux-libc5/2.7.2.1/include \
-L /usr/lib/gcc-lib/i486-linux-libc5/2.7.2.1 "$@"
Special thanks to Patrick Auge, Patrick Peck, Judi Romijn, Solofo Ramangalahy, Hubert Rappold, Brian Ross, and Severine Simon for their bugs reports and proposed solutions.
[Hubert Garavel]
The "rfl" (Request for License) command shipped with CADP 97b is not Year 2000 compliant. It generates prototype license files valid for years 1900-1901 instead of 2000-2001.
YEAR=`date +19%y`and replace it with the correct line:
YEAR=`date +%Y`
If you do not apply this patch, we will correct by hand the dates contained in the license file(s) you will send to us. By doing so, this Y2K problem should not be visible from you.
Warning: If you are using a Sparc station running SunOS 4.1.*, before installing CADP, you must have applied the appropriate "Year 2000" patches provided by Sun (www.sun.com). One of these patches updates the /bin/date command. The old (non-patched) /bin/date command does not accept the +%Y argument.
Back to the CADP Home Page