You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Linking with LLVM is heavy operation and for development, it would be good to not link LLVM to GazerLLVM module, rather only link (of course, still dynamically) to the main binary.
Plus this allows us to use LLVM's opt utility which is useful for debugging. (opt already links LLVM: the error is similar to this: ziglang/zig#67 )
The text was updated successfully, but these errors were encountered:
ghost
changed the title
Improve link time
Rethink building procedure
Sep 2, 2020
Only gazer-bmc uses GazerZ3Solver, but disabling it does not work. (update: Also, GazerVerifier is used only in gazer-bmc)
gazer-bmc, gazer-theta and gazer-cfa functional tests could be split to test only portion of the code.
GazerLLVM linkage is a heavy operation because of the big LLVM library (libraries, to be exact). This could be added at the last build stage, if I'm not mistaken.
Z3Solver is downloaded (or at least the version is checked online) at every make invocation, which is too heavy for an iterative build system.
I'm not too familiar with the CMake build system, I'll try play around a bit to speed up the process (mainly for the iterative building)
Linking with LLVM is heavy operation and for development, it would be good to not link LLVM to GazerLLVM module, rather only link (of course, still dynamically) to the main binary.
Plus this allows us to use LLVM's
opt
utility which is useful for debugging. (opt already links LLVM: the error is similar to this: ziglang/zig#67 )The text was updated successfully, but these errors were encountered: