You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
95 lines
2.1 KiB
95 lines
2.1 KiB
2 years ago
|
# 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
|
||
|
|
}
|