blob: 9cc88ca7081d35825b432664b026ab26ec4c0fc5 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
{ lib
, stdenv
, fetchFromGitHub
, testers
, bison
, cadical
, cbmc
, cmake
, flex
, makeWrapper
, perl
}:
stdenv.mkDerivation rec {
pname = "cbmc";
version = "5.90.0";
src = fetchFromGitHub {
owner = "diffblue";
repo = pname;
rev = "${pname}-${version}";
sha256 = "sha256-c6Ms/IStmKug5nz37TzjeexkY3YfWaUqEKIC2viMK9g=";
};
nativeBuildInputs = [
bison
cmake
flex
perl
makeWrapper
];
buildInputs = [ cadical ];
# do not download sources
# link existing cadical instead
patches = [
./0001-Do-not-download-sources-in-cmake.patch
];
postPatch = ''
# do not hardcode gcc
substituteInPlace "scripts/bash-autocomplete/extract_switches.sh" \
--replace "gcc" "$CC" \
--replace "g++" "$CXX"
# fix library_check.sh interpreter error
patchShebangs .
'' + lib.optionalString (!stdenv.cc.isGNU) ''
# goto-gcc rely on gcc
substituteInPlace "regression/CMakeLists.txt" \
--replace "add_subdirectory(goto-gcc)" ""
'';
postInstall = ''
# goto-cc expects ls_parse.py in PATH
mkdir -p $out/share/cbmc
mv $out/bin/ls_parse.py $out/share/cbmc/ls_parse.py
chmod +x $out/share/cbmc/ls_parse.py
wrapProgram $out/bin/goto-cc \
--prefix PATH : "$out/share/cbmc" \
'';
env.NIX_CFLAGS_COMPILE = toString (lib.optionals stdenv.cc.isGNU [
# Needed with GCC 12 but breaks on darwin (with clang)
"-Wno-error=maybe-uninitialized"
] ++ lib.optionals stdenv.cc.isClang [
# fix "argument unused during compilation"
"-Wno-unused-command-line-argument"
]);
# TODO: add jbmc support
cmakeFlags = [ "-DWITH_JBMC=OFF" "-Dsat_impl=cadical" "-Dcadical_INCLUDE_DIR=${cadical.dev}/include" ];
passthru.tests.version = testers.testVersion {
package = cbmc;
command = "cbmc --version";
};
meta = with lib; {
description = "CBMC is a Bounded Model Checker for C and C++ programs";
homepage = "http://www.cprover.org/cbmc/";
license = licenses.bsdOriginal;
maintainers = with maintainers; [ jiegec ];
platforms = platforms.unix;
# https://github.com/diffblue/cbmc/issues/7423
broken = stdenv.isLinux && stdenv.isAarch64;
};
}
|