[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] PVS 3.2 on Fedora Core 5



Hello,

I had a little trouble installing PVS 3.2 on Fedora Core 5 today.  Here's where I started:

-Download and install 5 CD ISO images containing Fedora Core 5 (FC5)
-Tweak with network card and display settings on FC5
-Update all software using "yum -y update" at command line in FC5
-Install emacs using "yum install emacs"
-Install PVS 3.2 from the linux zip and the system zip
-Relocate PVS using bin/relocate

My problem was that when I ran the pvs shell script to start up PVS, I received some errors stating that low-level glibc shared objects could not be used / found.  Errors included:

uname: errror while loading shared libraries: libc.so.6: cannot open shared object file: No such file or directory

and:

/bin/sh: error while loading shared libraries: libdl.so.2: cannot open shared object file: No such file or directory

After some script debugging, I found that these errors occurred after the pvs shell script had exported the shell variable LD_ASSUME_KERNEL.  Google helped me to understand what that meant, see

http://people.redhat.com/drepper/assumekernel.html (technical overview) and
http://dag.wieers.com/howto/compatibility/ (simpler How-to advice)

Next I experimented with modifications the pvs script.  I chose to run the emacs editor (using the installed PVS extensions) using the "one time" method described by Dag Wieers's compatibility webpage as follows:

PVSEMACS="LD_ASSUME_KERNEL=${LD_ASSUME_KERNEL} ${PVSEMACS}"

I inserted this line at a carefully chosen place within the pvs script.  Please note that the location of this line within the pvs script MUST be chosen carefully.  I chose to put it directly after these lines:

case $PVSEMCAS in
  *[xl]emacs*) \

I think this solved my problem.  This fix enabled me to launch pvs within the emacs editor using the (modified) pvs script, and parse, typecheck and prove the example from chapter 2 of the PVS system guide -- hopefully that means it works Ok.

Best regards,

Mark Brown
RedPhone Security