blob: f4b0b0eea17f133415d9ce5fb203825528a5bb1d (
plain)
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
89
90
91
92
93
94
|
# Copyright 1999-2022 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
DOTNET_COMPAT=6.0
inherit edo multiprocessing
DESCRIPTION="SMT-based program verifier"
HOMEPAGE="https://github.com/boogie-org/boogie/"
SRC_URI="
https://github.com/boogie-org/${PN}/archive/v${PV}.tar.gz
-> ${P}.tar.gz
https://dev.gentoo.org/~xgqt/distfiles/deps/${PN}-2.15.8-deps.tar.xz
"
LICENSE="MIT"
SLOT="0"
KEYWORDS="~amd64"
IUSE="debug test"
RESTRICT="!test? ( test )"
BDEPEND="virtual/dotnet-sdk:${DOTNET_COMPAT}"
RDEPEND="
${BDEPEND}
sci-mathematics/z3
"
BDEPEND+="
test? (
dev-python/lit
dev-python/OutputCheck
)
"
# Generated by dotnet.
QA_PREBUILT="/usr/share/boogie/BoogieDriver"
src_prepare() {
export DOTNET_CLI_TELEMETRY_OPTOUT=1
export DOTNET_NOLOGO=1
export DOTNET_CONFIGURATION=$(usex debug Debug Release)
export DOTNET_OUTPUT="${WORKDIR}"/${P}_net${DOTNET_COMPAT}_${DOTNET_CONFIGURATION}/${PN}
export NUGET_PACKAGES="${WORKDIR}"/${PN}-2.15.8/Source/nuget_packages
default
# Remove bad tests.
local bad_tests=(
civl/inductive-sequentialization/BroadcastConsensus.bpl
livevars/bla1.bpl
prover/cvc5.bpl
test0/MaxKeepGoingSplits.bpl
test15/CaptureInlineUnroll.bpl
test15/CaptureState.bpl
test15/CommonVariablesPruning.bpl
)
local bad_test
for bad_test in ${bad_tests[@]} ; do
rm "${S}"/Test/${bad_test} || die
done
# Update the boogieBinary variable.
sed "/^boogieBinary/s|= .*|= '${DOTNET_OUTPUT}/BoogieDriver.dll'|" \
-i "${S}"/Test/lit.site.cfg || die "failed to update lit.site.cfg"
}
src_configure() {
edob dotnet restore "${S}"/Source \
--source "${NUGET_PACKAGES}" -p:TargetFramework=net${DOTNET_COMPAT}
}
src_compile() {
local myopts=(
--configuration ${DOTNET_CONFIGURATION}
--no-restore
--no-self-contained
--nologo
--output "${DOTNET_OUTPUT}"
-consoleLoggerParameters:ErrorsOnly
-maxCpuCount:$(makeopts_jobs)
)
edob dotnet build ${myopts[@]} "${S}"/Source
}
src_test() {
lit "${S}"/Test || die "tests failed"
}
src_install() {
mkdir -p "${ED}"/usr/share/ || die
cp -r "${DOTNET_OUTPUT}" "${ED}"/usr/share/ || die
dosym -r /usr/share/${PN}/BoogieDriver /usr/bin/boogie
}
|
