projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 34798fb) | patch
Refactor our integration of LFSC (#6201)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 24 Mar 2021 15:07:15 +0000 (16:07 +0100)
committerGitHub <noreply@github.com>
Wed, 24 Mar 2021 15:07:15 +0000 (10:07 -0500)
commit31bba4ba83354f41c756e9800489672ff1c9711c
treea9a7d07d93b6e80d4b6c9e273b3f3c1ebdb2d4c6tree
parent34798fb86eabe7b9aaff86be23a7a3428ebfc957commit | diff
Refactor our integration of LFSC (#6201)

This PR further decouples LFSC from the remaining build system, but makes it more convenient to use at the same time.
The contrib/get-lfsc-checker script is now completely standalone and installs LFSC and the necessary signatures to deps/, as well as wrapper scripts to conveniently run lfscc from there and directly check cvc4 proofs.
The goal would be to automatically use LFSC in our regressions as well.
cmake/FindLFSC.cmake diff | blob | history
contrib/get-lfsc-checker diff | blob | history
contrib/lfsc_lsan.supp [deleted file] blob | history