Build issue, x86_64, Fedora

[clementblaudeau]

After getting the latest sbcl,

> sbcl --version
SBCL 2.5.10

I tried doing ./configure then ./make.

> ./configure
checking build system type... x86_64-pc-linux-gnu
checking pvspath... found "/home/username/PVS/pvs.in"
checking for gcc... gcc
checking whether the C compiler works... yes
checking for C compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether the compiler supports GNU C... yes
checking whether gcc accepts -g... yes
checking for gcc option to enable C11 features... none needed
checking for ld... ld
checking for ar... ar
checking for ranlib... ranlib
checking for grep... grep
checking for mkdir... mkdir
checking for a race-free mkdir -p... /usr/bin/mkdir -p
checking for tar... tar
checking for rm... rm
checking for curl... curl
checking for git... git
checking for sbcl... sbcl
configure: creating ./config.status
config.status: creating Makefile
config.status: creating pvs
config.status: creating pvsio
config.status: creating proveit
config.status: creating provethem
config.status: creating pvs-get-patches
config.status: creating doc/api/Makefile
config.status: creating doc/user-guide/Makefile
config.status: creating doc/language/Makefile
config.status: creating doc/language/pvs-doc.el
config.status: creating doc/prover/Makefile
config.status: creating lib/registry.conf

However, it stops on this error :

make[1]: Leaving directory '/home/username/PVS/src/BDD/ix86_64-Linux'
error output:
../mu_interface.c: In function ‘mu___modelcheck_formula’:
../mu_interface.c:217:14: error: too many arguments to function ‘modelcheck_formula’; expected 0, have 1
  217 |    mcvalue = modelcheck_formula(fml);
      |              ^~~~~~~~~~~~~~~~~~ ~~~
../mu_interface.c:206:18: note: declared here
  206 |    extern BDDPTR modelcheck_formula();
      |                  ^~~~~~~~~~~~~~~~~~
../mu_interface.c: In function ‘bdd___bdd_sum_of_cubes’:
../mu_interface.c:235:14: error: too many arguments to function ‘bdd_sum_of_cubes’; expected 0, have 2
  235 |    mcvalue = bdd_sum_of_cubes (f, irredundant);
      |              ^~~~~~~~~~~~~~~~  ~
../mu_interface.c:224:20: note: declared here
  224 |    extern BDD_LIST bdd_sum_of_cubes();
      |                    ^~~~~~~~~~~~~~~~
../mu_interface.c: At top level:
../mu_interface.c:240:8: error: conflicting types for ‘modelcheck_formula’; have ‘struct bdd *(struct _Formula *)’
  240 | BDDPTR modelcheck_formula (Formula fml)
      |        ^~~~~~~~~~~~~~~~~~
../mu_interface.c:206:18: note: previous declaration of ‘modelcheck_formula’ with type ‘struct bdd *(void)’
  206 |    extern BDDPTR modelcheck_formula();
      |                  ^~~~~~~~~~~~~~~~~~
make[1]: *** [Makefile:22: mu_interface.o] Error 1

Type HELP for debugger help, or (SB-EXT:EXIT) to exit from SBCL.

restarts (invokable by number or by possibly-abbreviated name):
  0: [RETRY                        ] Retry
                                     completing load for #<MODULE "pvs" "bddlib">.
  1: [ACCEPT                       ] Continue, treating
                                     completing load for #<MODULE "pvs" "bddlib">
                                     as having been successful.
  2:                                 Retry ASDF operation.
  3: [CLEAR-CONFIGURATION-AND-RETRY] Retry ASDF operation after resetting the
                                     configuration.
  4:                                 Retry ASDF operation.
  5:                                 Retry ASDF operation after resetting the
                                     configuration.
  6: [CONTINUE                     ] Ignore runtime option --eval "(asdf:operate :program-op :pvs)".
  7: [ABORT                        ] Skip rest of --eval and --load options.
  8:                                 Skip to toplevel READ/EVAL/PRINT loop.
  9: [EXIT                         ] Exit SBCL (calling #'EXIT, killing the process).

(PVS::MAKE-IN-PLATFORM #<unavailable argument> #<unavailable argument> #<unused argument>)
   source: (ERROR "Failure in ~a:~%output:~%~a~%error output:~%~a" MAKE-CMD
                  OUT-STR ERR-STR)
0] 

I'm on Fedora 42

Linux hostname 6.16.10-200.fc42.x86_64 #1 SMP PREEMPT_DYNAMIC Thu Oct  2 19:23:55 UTC 2025 x86_64 GNU/Linux

Am I missing something on the installation instructions ? Do you have a workaround for this issue ?

On a more general note, I'd like to continue working on a project started with pvs7.1-allegro, should I try using pvs8-sbcl or will I run into incompatibilities ?

[enshankar]

Clement: Try it now.  It looks like some C compilers are particular about having the arguments in extern signature. Best, Shankar

…

On 11/24/25 10:30 AM, Clément Blaudeau wrote: *clementblaudeau* created an issue (SRI-CSL/PVS#102) <#102> After getting the latest sbcl, > sbcl --version SBCL 2.5.10 I tried doing |./configure| then |./make|. > ./configure checking build system type... x86_64-pc-linux-gnu checking pvspath... found"/home/username/PVS/pvs.in" checkingfor gcc... gcc checking whether the C compiler works... yes checkingfor C compiler default output file name... a.out checkingfor suffix of executables... checking whether we are cross compiling... no checkingfor suffix of object files... o checking whether the compiler supports GNU C... yes checking whether gcc accepts -g... yes checkingfor gcc option toenable C11 features... none needed checkingfor ld... ld checkingfor ar... ar checkingfor ranlib... ranlib checkingfor grep... grep checkingfor mkdir... mkdir checkingfor a race-free mkdir -p... /usr/bin/mkdir -p checkingfor tar... tar checkingfor rm... rm checkingfor curl... curl checkingfor git... git checkingfor sbcl... sbcl configure: creating ./config.status config.status: creating Makefile config.status: creating pvs config.status: creating pvsio config.status: creating proveit config.status: creating provethem config.status: creating pvs-get-patches config.status: creating doc/api/Makefile config.status: creating doc/user-guide/Makefile config.status: creating doc/language/Makefile config.status: creating doc/language/pvs-doc.el config.status: creating doc/prover/Makefile config.status: creating lib/registry.conf However, it stops on this error : make[1]: Leaving directory'/home/username/PVS/src/BDD/ix86_64-Linux' error output: ../mu_interface.c: Infunction ‘mu___modelcheck_formula’: ../mu_interface.c:217:14: error: too many arguments tofunction ‘modelcheck_formula’; expected 0, have 1 217| mcvalue = modelcheck_formula(fml); | ^~~~~~~~~~~~~~~~~~~~~ ../mu_interface.c:206:18: note: declared here 206| extern BDDPTRmodelcheck_formula(); | ^~~~~~~~~~~~~~~~~~ ../mu_interface.c: Infunction ‘bdd___bdd_sum_of_cubes’: ../mu_interface.c:235:14: error: too many arguments tofunction ‘bdd_sum_of_cubes’; expected 0, have 2 235| mcvalue = bdd_sum_of_cubes (f, irredundant); | ^~~~~~~~~~~~~~~~~ ../mu_interface.c:224:20: note: declared here 224| extern BDD_LISTbdd_sum_of_cubes(); | ^~~~~~~~~~~~~~~~ ../mu_interface.c: At top level: ../mu_interface.c:240:8: error: conflicting typesfor ‘modelcheck_formula’; have ‘struct bdd*(struct _Formula*)’ 240| BDDPTR modelcheck_formula (Formula fml) | ^~~~~~~~~~~~~~~~~~ ../mu_interface.c:206:18: note: previous declaration of ‘modelcheck_formula’ withtype ‘struct bdd*(void)’ 206| extern BDDPTRmodelcheck_formula(); | ^~~~~~~~~~~~~~~~~~ make[1]:*** [Makefile:22: mu_interface.o] Error 1 Type HELPfor debugger help, or (SB-EXT:EXIT) toexit from SBCL. restarts (invokable by number or by possibly-abbreviated name): 0: [RETRY ] Retry completing loadfor #<MODULE "pvs" "bddlib">. 1: [ACCEPT ] Continue, treating completing loadfor #<MODULE "pvs" "bddlib"> as having been successful. 2: Retry ASDF operation. 3: [CLEAR-CONFIGURATION-AND-RETRY] Retry ASDF operation after resetting the configuration. 4: Retry ASDF operation. 5: Retry ASDF operation after resetting the configuration. 6: [CONTINUE ] Ignore runtime option --eval"(asdf:operate :program-op :pvs)". 7: [ABORT ] Skip rest of --eval and --load options. 8: Skip to toplevel READ/EVAL/PRINT loop. 9: [EXIT ] Exit SBCL (calling#'EXIT, killing the process). (PVS::MAKE-IN-PLATFORM#<unavailable argument> #<unavailable argument> #<unused argument>) source: (ERROR"Failure in ~a:~%output:~%~a~%error output:~%~a" MAKE-CMD OUT-STR ERR-STR) 0] I'm on Fedora 42 Linux hostname 6.16.10-200.fc42.x86_64#1 SMP PREEMPT_DYNAMIC Thu Oct 2 19:23:55 UTC 2025 x86_64 GNU/Linux Am I missing something on the installation instructions ? Do you have a workaround for this issue ? On a more general note, I'd like to continue working on a project started with pvs7.1-allegro, should I try using pvs8-sbcl or will I run into incompatibilities ? — Reply to this email directly, view it on GitHub <#102>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA2DUCNDQZQFSGK655ZGPKD36NFDHAVCNFSM6AAAAACNBZ46MOVHI2DSMVQWIX3LMV43ASLTON2WKOZTGY3DAMBVHE4DGNY>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[clementblaudeau]

Hi Shankar,
Thank you for the fix! I still get an error, but different:

error output:
../bdd/utils/double.c: In function ‘D_sprintf’:
../bdd/utils/double.c:519:7: warning: this ‘if’ clause does not guard... [-Wmisleading-indentation]
  519 |       if (!((mantissa1 = D_L_MANTISSA (d)) == 1) || !D_EXP (d))
      |       ^~
../bdd/utils/double.c:521:44: note: ...this statement, but the latter is misleadingly indented as if it were guarded by the ‘if’
  521 |       sprintf (p, "%u", D_L_MANTISSA (d)); while (*p) p++;
      |                                            ^~~~~
../bdd/utils/double.c:523:3: warning: this ‘if’ clause does not guard... [-Wmisleading-indentation]
  523 |   if (D_EXP (d))
      |   ^~
../bdd/utils/double.c:525:61: note: ...this statement, but the latter is misleadingly indented as if it were guarded by the ‘if’
  525 |     sprintf (p, "%s2^%u", mantissa1 ? "" : "*", D_EXP (d)); while (*p) p++;
      |                                                             ^~~~~
In file included from /usr/include/bits/libc-header-start.h:33,
                 from /usr/include/stdio.h:28,
                 from ../bdd/utils/hash.c:15:
/usr/include/features.h:199:3: warning: #warning "_BSD_SOURCE and _SVID_SOURCE are deprecated, use _DEFAULT_SOURCE" [-Wcpp]
  199 | # warning "_BSD_SOURCE and _SVID_SOURCE are deprecated, use _DEFAULT_SOURCE"
      |   ^~~~~~~
../bdd/utils/hash.c: In function ‘hashtab_full_handler’:
../bdd/utils/hash.c:298:10: error: too many arguments to function ‘tab->rehash_function’; expected 0, have 2
  298 |         (*(tab->rehash_function)) (i, newi);
      |         ~^~~~~~~~~~~~~~~~~~~~~~~~  ~
In file included from ../bdd/utils/hash.c:21:
../bdd/utils/hash.h:74:10: note: declared here
   74 |   void (*rehash_function) ();   /* function called when non-NULL */
      |          ^~~~~~~~~~~~~~~
make[1]: *** [Makefile:22: hash.o] Error 1

Type HELP for debugger help, or (SB-EXT:EXIT) to exit from SBCL.

restarts (invokable by number or by possibly-abbreviated name):
  0: [RETRY                        ] Retry
                                     completing load for #<MODULE "pvs" "bddlib">.
  1: [ACCEPT                       ] Continue, treating
                                     completing load for #<MODULE "pvs" "bddlib">
                                     as having been successful.
  2:                                 Retry ASDF operation.
  3: [CLEAR-CONFIGURATION-AND-RETRY] Retry ASDF operation after resetting the
                                     configuration.
  4:                                 Retry ASDF operation.
  5:                                 Retry ASDF operation after resetting the
                                     configuration.
  6: [CONTINUE                     ] Ignore runtime option --eval "(asdf:operate :program-op :pvs)".
  7: [ABORT                        ] Skip rest of --eval and --load options.
  8:                                 Skip to toplevel READ/EVAL/PRINT loop.
  9: [EXIT                         ] Exit SBCL (calling #'EXIT, killing the process).

(PVS::MAKE-IN-PLATFORM #<unavailable argument> #<unavailable argument> #<unused argument>)
   source: (ERROR "Failure in ~a:~%output:~%~a~%error output:~%~a" MAKE-CMD
                  OUT-STR ERR-STR)

Any ideas where it could come from ?
Best,
Clément

[karthiknukala]

Hi Clement,

Just a little update - we're working on the bug but it's breaking functionality in unexpected places.

The fix is to fully qualify the arguments to function pointers stored in structs (in the src/BDD C files).

For example, for that declaration in hash.h, the fix is to update
void (*rehash_function)();
to
void (*rehash_function)(int old_index, int new_index);

There are a few other locations where this pattern appears.

I'll keep you posted as I make progress on fixing this bug and I'll let you know once it's merged in.

Regards,
Karthik Nukala

[clementblaudeau]

Thank you very much for the update.
Is it linked to Fedora somehow, or would it be the same on all distributions ? How are you installing PVS on your machine, if not with the normal workflow ? Should I try an older version ?

[karthiknukala]

Hi Clement,

What version of C/gcc are you using?

The BDD package happens to be pretty old (early/mid-90s) and given that modern compilers are a little less permissive, should be updated accordingly. A big distinction between K&R C and ANSI C is that the latter introduces function prototypes and while most compilers have largely been backwards compatible, there is still that variability between compilers (and versions of those compilers).

I happen to be on a Mac, following the normal workflow.

gcc --version
Apple clang version 17.0.0 (clang-1700.4.4.1)
Target: arm64-apple-darwin24.6.0
Thread model: posix
InstalledDir: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin

I plan on testing my fixes later tonight on my Linux machine. I'll add an update here then.

An immediate workaround would be to fix the line manually (in src/BDD/bdd/utils/hash.h).

Regards,
Karthik Nukala

[karthiknukala]

Hi Clement,

Pushed a fix (commit e867097) - please give this a try and let me know if you run into any further issues.

Regards,
Karthik Nukala