search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
822 stars 259 forks source link

Cannot build with IPASIR - cryptominisat #5345

Closed jmony closed 3 years ago

jmony commented 4 years ago

CBMC version: master and Release 5.12 Operating system: Linux (Debian and Ubuntu) Exact command line resulting in the issue: make -C src IPASIR=/home/ubuntu/cryptominisat/src LIBS="/home/ubuntu/cryptominisat/build/lib/libipasircryptominisat5.a" (cryptominisat built OK) What behaviour did you expect: Successful build What happened instead:

Entering solvers

make -C solvers make[1]: Entering directory '/home/ubuntu/cbmc-cbmc-5.12/src/solvers' g++ -c -DHAVE_IPASIR -DSTDC_FORMAT_MACROS -DSTDC_LIMIT_MACROS -MMD -MP -std=c++11 -O2 -DHAVE_IPASIR -I .. -I /home/ubuntu/cryptominisat/src -o sat/satcheck_ipasir.o sat/satcheck_ipasir.cpp sat/satcheck_ipasir.cpp: In constructor ‘satcheck_ipasirt::satcheck_ipasirt()’: sat/satcheck_ipasir.cpp:161:36: error: no matching function for call to ‘cnf_solvert::cnf_solvert()’ satcheck_ipasirt::satcheck_ipasirt() ^ In file included from sat/satcheck_ipasir.h:15:0, from sat/satcheck_ipasir.cpp:20: sat/cnf.h:72:12: note: candidate: cnf_solvert::cnf_solvert(message_handlert&) explicit cnf_solvert(message_handlert &message_handler) ^~~ sat/cnf.h:72:12: note: candidate expects 1 argument, 0 provided sat/cnf.h:69:7: note: candidate: cnf_solvert::cnf_solvert(const cnf_solvert&) class cnf_solvert:public cnft ^~~ sat/cnf.h:69:7: note: candidate expects 1 argument, 0 provided sat/cnf.h:69:7: note: candidate: cnf_solvert::cnf_solvert(cnf_solvert&&) sat/cnf.h:69:7: note: candidate expects 1 argument, 0 provided ../common:222: recipe for target 'sat/satcheck_ipasir.o' failed make[1]: [sat/satcheck_ipasir.o] Error 1 make[1]: Leaving directory '/home/ubuntu/cbmc-cbmc-5.12/src/solvers' Makefile:97: recipe for target 'solvers.dir' failed make: [solvers.dir] Error 2 make: Leaving directory '/home/ubuntu/cbmc-cbmc-5.12/src'

jmony commented 4 years ago

I forgot to mention that I edited config.inc to uncomment IPASIR (and only IPASIR).

peterschrammel commented 4 years ago

This might be fixed by https://github.com/diffblue/cbmc/pull/5305.

jmony commented 4 years ago

I tried with #5305 but it had no effect.

tautschnig commented 3 years ago

I actually messed this up in 89641a2b47b8. We'll need #5305 (or some variant thereof) plus an additional fix.