search

ftsrg / gazer

An LLVM-based formal verification frontend for C programs.
24 stars 5 forks source link

Rework build process to allow integration of LLVM tools #94

Open radl97 opened 3 years ago

radl97 commented 3 years ago

This PR contains the first patch aiming to allow usage of LLVM tools (mostly opt) in the project.

Usage of opt would enable single pass tests, or later, even remove most, if not all driver (pass management) code.

It seems to me that if the build process got faster, however, it is partly because the shared libraries are not linked together (instead, the shared lib GazerLLVM.so knows all the modules used in the build process).

radl97 commented 3 years ago

I'd really like your input here, @sallaigy, if you have any experience, and whether this path is OK for us. Because we only have 5 or so shared libraries, it could be OK, I think.

sonarcloud[bot] commented 3 years ago

Kudos, SonarCloud Quality Gate passed!

Bug A 0 Bugs
Vulnerability A 0 Vulnerabilities
Security Hotspot A 0 Security Hotspots
Code Smell A 0 Code Smells

No Coverage information No Coverage information
No Duplication information No Duplication information

radl97 commented 3 years ago

Maybe it's best to describe the changes: Using LLVM's add_llvm_library, opt can be used. Somewhy I failed to bootstrap opt otherwise...

However the library (GazerLLVMBase) will only consist of links to the other libs (GazerAutomaton, etc.). I was unable to find out why, but all libs are searched at ../lib/. This is where LLVM usually stores its' modules, so it seems reasonable.