Opened 5 years ago

Closed 5 years ago

#71 closed defect (fixed)

Divine 4.3.2 Build failures

Reported by: imartisko Owned by: mornfall
Priority: major Milestone: 4.3
Component: other Keywords:
Cc: jamartis@…, kdudka@…



I am trying to build the stable version of divine on Fedora 29 but I am running into two problems.

1) The LLVM_CMAKE_PATH variable in the clang/lib/basic/cmakelist.txt does not seem to be set properly during the build which causes the build to fail. When I hardcode the absolute path to llvm/cmake/modulesGetSVN.cmake, the build continues

2) The build fails during the final linking with the error message in the attached file. This only happens when I'm trying to build the release flavour (make release). When building the debug flavour, the build completes successfully.

Attachments (2)

error (5.4 KB) - added by imartisko 5 years ago.
disable-VC-checks.patch (1.5 KB) - added by imartisko 5 years ago.

Download all attachments as: .zip

Change History (5)

Changed 5 years ago by imartisko

Attachment: error added

comment:1 Changed 5 years ago by mornfall

The error from 2) is fixed in the 'next' branch. If you do not want to pull it with darcs, you can apply the following diff locally:

patch c4cc63bfafe279bfb73c1fb8e10b1f837cee5656
Author: Petr Rockai <>
Date:   Tue Jul  2 11:40:13 CEST 2019
  * VM: Fix undefined references to context methods (release builds were affected).
diff -rN -u -p old-work/divine/vm/eval.hpp new-work/divine/vm/eval.hpp
--- old-work/divine/vm/eval.hpp	2019-07-02 16:43:36.735786387 +0200
+++ new-work/divine/vm/eval.hpp	2019-07-02 16:43:36.735786387 +0200
@@ -23,6 +23,7 @@
 #include <divine/vm/program.hpp>
 #include <divine/vm/value.hpp>
 #include <divine/vm/context.hpp>
+#include <divine/vm/ctx-debug.tpp>
 #include <divine/vm/divm.h>

As for 1), what is the version of 'cmake' that you are using? Do you have some sort of version control checkout that's not darcs? Seems like the module is only used if version control files exist (which normally don't).

comment:2 Changed 5 years ago by imartisko

Thanks for the patch, it seems to fix the issue 2). As for the issue 1), I have a git repo in the parent directory which seems to indeed be the cause of the problems. I've created a patch that introduces Makefile variable which disables these VC checks if needed (for the tarball versions of the divine, these checks should not be needed, I suppose).

Changed 5 years ago by imartisko

Attachment: disable-VC-checks.patch added

comment:3 Changed 5 years ago by mornfall

Resolution: fixed
Status: newclosed

I have disabled the VC checks unconditionally (we never actually want them anyway).

Note: See TracTickets for help on using tickets.