summaryrefslogtreecommitdiff
path: root/dev-lang/boogie
diff options
context:
space:
mode:
Diffstat (limited to 'dev-lang/boogie')
-rw-r--r--dev-lang/boogie/Manifest2
-rw-r--r--dev-lang/boogie/boogie-3.2.0.ebuild306
2 files changed, 308 insertions, 0 deletions
diff --git a/dev-lang/boogie/Manifest b/dev-lang/boogie/Manifest
index 4975c536a93d..0a528fee2208 100644
--- a/dev-lang/boogie/Manifest
+++ b/dev-lang/boogie/Manifest
@@ -1,5 +1,6 @@
AUX boogie-3.0.4-disable-analyzers.patch 764 BLAKE2B 965f6a8007a4324aa95b165109dcbc85f7bba5696d04772c53cfb1e456d0c60d2d3dce9103df641fe7f565d2a2d4e04a5d02aba43ac1ccc4527dcaae90b7b28b SHA512 b8c7b9172cd2f45be84058babd33c75f37dcb08f6c1a0b7c79b0ae2bd8afec70b29886f23d0a5553a00e1d3761a7788db0444d06788ee32aed2d1c2cd7cb9554
DIST boogie-3.1.6.tar.gz 2053303 BLAKE2B bc4c9ee72e605b1c78140f6120d0fe8ffcad663638829b28e8b5c7238d7265c156ad8994f4bb79989aea030b571b261f71b09050d80ab5a94625e47adc29a74d SHA512 31c4ca25bde610354f5ce4aaeab8f885c89f443a2d96671d55b4b38dc5dc30b6060f89100dba68a2bc962d6169618e1ab9f6958b1f12730687fa1e5c47267663
+DIST boogie-3.2.0.tar.gz 2064238 BLAKE2B 01b10f33dddd651b97786c0d9e3c8678c2c3afeb7dfc9403024a6d676b6b8a553b79804fe060b3e165f5b7dcee48de9f208639b115e5557fcd447f767f9144f0 SHA512 0642a407e0a7129776cbee934c45dbac0d12c41d9c920c6d2006c93af71046db0519b2530052686e5fc965a4b525641b5da1ab8ffeb4a48a3e8cfd5f918a6d66
DIST microsoft.bcl.asyncinterfaces.6.0.0.nupkg 76354 BLAKE2B aca3f5db71e4037dbdd604aeaebcd0962ccc171915b77b4c409ab744bf0a469c7d588f9504fc7fa49e3863e9593b66b4083235cb49e812d1f87b3dadb32e6003 SHA512 221a05a0c910f7a87b620d8f3831ed392b4eb95d112bee274d35f27009ad2a26445de9d7cd235fe6fb4a03f2550874bda3be3dddd96edaf9c0852a9c23d7b099
DIST microsoft.codecoverage.16.2.0.nupkg 3133582 BLAKE2B 418cf403247d594cde0d827f8ca8690019a7631525f07993937085f4bbf8473364b4c99aea6e8b7b0020208d15fe0da63f0f4e69c273493c51ae011e8bd82667 SHA512 91f1d43fc038a20f5367d9aab669105dc7514dfbe749260b52789c09a75abcc6bdc000ee0c7f432231d4cc09e99bf5b863dd6289d813342f74d9dad23a651625
DIST microsoft.csharp.4.0.1.nupkg 462346 BLAKE2B 209ccebc9103b803d26ea1f0232245c3cd231078b03a83a0011a2a79a1a8a324a72c5b3fda94b2686fff170932f366e165f81a36a70df590a39c45d70778e4be SHA512 c0e75a9162f28ba4c4572c8fac4fd4c8c97d6d3505a37683646ba5f7e5f6ac0da69d5200d2646054de90e8e08f893a10e514591b69b8273640842b2cf90bddec
@@ -191,4 +192,5 @@ DIST system.xml.xpath.4.3.0.nupkg 250182 BLAKE2B 8a4177d47af56bc7a6289ed8f2cac41
DIST system.xml.xpath.xmldocument.4.0.1.nupkg 86933 BLAKE2B 4c03b5a9433c2c954e75d212f9026885aa7514574b73a54880c3d55baee6bd5517abb46b67b22b9b6e63de92a8bc5ab4ff37e3f7e6454a5c5137ae2be6574b75 SHA512 81041a08d3b9158c43dfb48d42f13ec9950d7c2b7f63e1600a779a77786edfb46c522c32d9cc6a44358fbfe11efba0e539e578ef169261867a1905b8121a045d
DIST system.xml.xpath.xmldocument.4.3.0.nupkg 138523 BLAKE2B ba53f3b5ac0f2d1d1e9120940b302e6960690ed4a44b96ba15b03e16f9159f2c57d6004aa55b796ba2327009d23fc2f10d4d09e948b88eb6af36efa5f76e401b SHA512 f75b6f7c75874ab6053e8942c1662a6e9a3561aa01502437b8d67f3bfcebd1ebf906792801326889ed7acb094c55469766d7d27cd10bc61b46ddaaa94dfc11e3
EBUILD boogie-3.1.6.ebuild 9418 BLAKE2B f2ab18943dd53d9d54fbf579d6f603ff53c3c74ab0e373c8be244b91cb172c964d01970400f8096a6fd16d1a9838df7d4d1597f62e74b2ab345e4d24410bac41 SHA512 28a0a1089b99108b86ff165c1157294b6cb7562f775a9b78420caa2ad925c7620b9e6faa3318279dd07da3c5da44886794cc9187484549aa921d6ab7aae1a7b2
+EBUILD boogie-3.2.0.ebuild 9475 BLAKE2B 1c2fc5631b2f16ee7c55cf850e35add9cc8e6f83271b9dbe89cd3ae91eef04068bf1eba0585dbbbb751a2e08740ba2f60492f9dc1fd169a9211b29939693c00d SHA512 4dda5316e21247409c0568fc13ff9572c6f01a4ce1be50db002fd4d68ab49ef8795213c097511c3d674de7fb52cd860243cbcd859e64ae13474e2dfa77d96d84
MISC metadata.xml 1102 BLAKE2B 215544658792715aae72787f7c949ed89df9c05ceab5a919a861c02b7938c0d1ee228e0ede55008287b616faf70992a8c1f2854e6e5e1fc909718ae682996bb8 SHA512 b6a626c485e2a5db3390da62c629507a60417eda8b508d7ed8d1c017ac337743d2c4fe0e8554b103f989176dcd2969cc8579e91532b07a22c1b66328ef241e8d
diff --git a/dev-lang/boogie/boogie-3.2.0.ebuild b/dev-lang/boogie/boogie-3.2.0.ebuild
new file mode 100644
index 000000000000..049cfbc87840
--- /dev/null
+++ b/dev-lang/boogie/boogie-3.2.0.ebuild
@@ -0,0 +1,306 @@
+# Copyright 1999-2024 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+DOTNET_PKG_COMPAT=8.0
+NUGETS="
+microsoft.bcl.asyncinterfaces@6.0.0
+microsoft.codecoverage@16.2.0
+microsoft.csharp@4.0.1
+microsoft.dotnet.internalabstractions@1.0.0
+microsoft.net.test.sdk@16.2.0
+microsoft.netcore.platforms@1.0.1
+microsoft.netcore.platforms@1.1.0
+microsoft.netcore.targets@1.0.1
+microsoft.netcore.targets@1.1.0
+microsoft.testplatform.objectmodel@16.2.0
+microsoft.testplatform.testhost@16.2.0
+microsoft.win32.primitives@4.0.1
+microsoft.win32.primitives@4.3.0
+microsoft.win32.registry@4.0.0
+microsoft.win32.registry@4.3.0
+microsoft.win32.systemevents@6.0.0
+netstandard.library@1.6.0
+netstandard.library@2.0.0
+newtonsoft.json@9.0.1
+nunit@3.12.0
+nunit3testadapter@3.15.1
+runtime.any.system.collections@4.3.0
+runtime.any.system.diagnostics.tools@4.3.0
+runtime.any.system.diagnostics.tracing@4.3.0
+runtime.any.system.globalization.calendars@4.3.0
+runtime.any.system.globalization@4.3.0
+runtime.any.system.io@4.3.0
+runtime.any.system.reflection.extensions@4.3.0
+runtime.any.system.reflection.primitives@4.3.0
+runtime.any.system.reflection@4.3.0
+runtime.any.system.resources.resourcemanager@4.3.0
+runtime.any.system.runtime.handles@4.3.0
+runtime.any.system.runtime.interopservices@4.3.0
+runtime.any.system.runtime@4.3.0
+runtime.any.system.text.encoding.extensions@4.3.0
+runtime.any.system.text.encoding@4.3.0
+runtime.any.system.threading.tasks@4.3.0
+runtime.any.system.threading.timer@4.3.0
+runtime.debian.8-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.fedora.23-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.fedora.24-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.native.system.io.compression@4.1.0
+runtime.native.system.net.http@4.0.1
+runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.native.system.security.cryptography@4.0.0
+runtime.native.system@4.0.0
+runtime.native.system@4.3.0
+runtime.opensuse.13.2-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.opensuse.42.1-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.osx.10.10-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.rhel.7-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.ubuntu.14.04-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.ubuntu.16.04-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.ubuntu.16.10-x64.runtime.native.system.security.cryptography.openssl@4.3.0
+runtime.unix.microsoft.win32.primitives@4.3.0
+runtime.unix.system.console@4.3.0
+runtime.unix.system.diagnostics.debug@4.3.0
+runtime.unix.system.io.filesystem@4.3.0
+runtime.unix.system.net.primitives@4.3.0
+runtime.unix.system.net.sockets@4.3.0
+runtime.unix.system.private.uri@4.3.0
+runtime.unix.system.runtime.extensions@4.3.0
+system.appcontext@4.1.0
+system.buffers@4.0.0
+system.buffers@4.3.0
+system.collections.concurrent@4.0.12
+system.collections.immutable@1.2.0
+system.collections.nongeneric@4.0.1
+system.collections.nongeneric@4.3.0
+system.collections.specialized@4.0.1
+system.collections.specialized@4.3.0
+system.collections@4.0.11
+system.collections@4.3.0
+system.componentmodel.eventbasedasync@4.0.11
+system.componentmodel.eventbasedasync@4.3.0
+system.componentmodel.primitives@4.1.0
+system.componentmodel.primitives@4.3.0
+system.componentmodel.typeconverter@4.1.0
+system.componentmodel.typeconverter@4.3.0
+system.componentmodel@4.0.1
+system.componentmodel@4.3.0
+system.configuration.configurationmanager@6.0.0
+system.console@4.0.0
+system.diagnostics.debug@4.0.11
+system.diagnostics.debug@4.3.0
+system.diagnostics.diagnosticsource@4.0.0
+system.diagnostics.process@4.1.0
+system.diagnostics.process@4.3.0
+system.diagnostics.textwritertracelistener@4.0.0
+system.diagnostics.tools@4.0.1
+system.diagnostics.tracesource@4.0.0
+system.diagnostics.tracing@4.1.0
+system.diagnostics.tracing@4.3.0
+system.drawing.common@6.0.0
+system.dynamic.runtime@4.0.11
+system.globalization.calendars@4.0.1
+system.globalization.extensions@4.0.1
+system.globalization.extensions@4.3.0
+system.globalization@4.0.11
+system.globalization@4.3.0
+system.io.compression.zipfile@4.0.1
+system.io.compression@4.1.0
+system.io.filesystem.primitives@4.0.1
+system.io.filesystem.primitives@4.3.0
+system.io.filesystem@4.0.1
+system.io.filesystem@4.3.0
+system.io@4.1.0
+system.io@4.3.0
+system.linq.async@6.0.1
+system.linq.expressions@4.1.0
+system.linq@4.1.0
+system.linq@4.3.0
+system.net.http@4.1.0
+system.net.nameresolution@4.3.0
+system.net.primitives@4.0.11
+system.net.sockets@4.1.0
+system.objectmodel@4.0.12
+system.private.datacontractserialization@4.1.1
+system.private.uri@4.3.0
+system.reactive@4.4.1
+system.reflection.emit.ilgeneration@4.0.1
+system.reflection.emit.lightweight@4.0.1
+system.reflection.emit@4.0.1
+system.reflection.extensions@4.0.1
+system.reflection.extensions@4.3.0
+system.reflection.metadata@1.3.0
+system.reflection.primitives@4.0.1
+system.reflection.primitives@4.3.0
+system.reflection.typeextensions@4.1.0
+system.reflection.typeextensions@4.3.0
+system.reflection@4.1.0
+system.reflection@4.3.0
+system.resources.resourcemanager@4.0.1
+system.resources.resourcemanager@4.3.0
+system.runtime.caching@6.0.0
+system.runtime.extensions@4.1.0
+system.runtime.extensions@4.3.0
+system.runtime.handles@4.0.1
+system.runtime.handles@4.3.0
+system.runtime.interopservices.runtimeinformation@4.0.0
+system.runtime.interopservices.runtimeinformation@4.3.0
+system.runtime.interopservices@4.1.0
+system.runtime.interopservices@4.3.0
+system.runtime.loader@4.0.0
+system.runtime.numerics@4.0.1
+system.runtime.serialization.json@4.0.2
+system.runtime.serialization.primitives@4.1.1
+system.runtime@4.1.0
+system.runtime@4.3.0
+system.security.accesscontrol@6.0.0
+system.security.claims@4.3.0
+system.security.cryptography.algorithms@4.2.0
+system.security.cryptography.cng@4.2.0
+system.security.cryptography.csp@4.0.0
+system.security.cryptography.encoding@4.0.0
+system.security.cryptography.openssl@4.0.0
+system.security.cryptography.primitives@4.0.0
+system.security.cryptography.protecteddata@6.0.0
+system.security.cryptography.x509certificates@4.1.0
+system.security.permissions@6.0.0
+system.security.principal.windows@4.3.0
+system.security.principal@4.3.0
+system.text.encoding.extensions@4.0.11
+system.text.encoding.extensions@4.3.0
+system.text.encoding@4.0.11
+system.text.encoding@4.3.0
+system.text.regularexpressions@4.1.0
+system.text.regularexpressions@4.3.0
+system.threading.tasks.extensions@4.0.0
+system.threading.tasks.extensions@4.3.0
+system.threading.tasks@4.0.11
+system.threading.tasks@4.3.0
+system.threading.thread@4.0.0
+system.threading.thread@4.3.0
+system.threading.threadpool@4.0.10
+system.threading.threadpool@4.3.0
+system.threading.timer@4.0.1
+system.threading@4.0.11
+system.threading@4.3.0
+system.windows.extensions@6.0.0
+system.xml.readerwriter@4.0.11
+system.xml.readerwriter@4.3.0
+system.xml.xdocument@4.0.11
+system.xml.xmldocument@4.0.1
+system.xml.xmldocument@4.3.0
+system.xml.xmlserializer@4.0.11
+system.xml.xpath.xmldocument@4.0.1
+system.xml.xpath.xmldocument@4.3.0
+system.xml.xpath@4.0.1
+system.xml.xpath@4.3.0
+"
+
+inherit check-reqs dotnet-pkg edo multiprocessing
+
+DESCRIPTION="SMT-based program verifier"
+HOMEPAGE="https://github.com/boogie-org/boogie/"
+
+if [[ "${PV}" == *9999* ]] ; then
+ inherit git-r3
+
+ EGIT_REPO_URI="https://github.com/boogie-org/${PN}.git"
+else
+ SRC_URI="https://github.com/boogie-org/${PN}/archive/v${PV}.tar.gz
+ -> ${P}.tar.gz"
+
+ KEYWORDS="~amd64"
+fi
+
+SRC_URI+=" ${NUGET_URIS} "
+
+LICENSE="MIT"
+SLOT="0"
+IUSE="test"
+RESTRICT="!test? ( test )"
+
+RDEPEND="
+ sci-mathematics/z3
+"
+BDEPEND="
+ ${RDEPEND}
+ test? (
+ dev-python/OutputCheck
+ dev-python/lit
+ dev-python/psutil
+ )
+"
+
+PATCHES=( "${FILESDIR}/${PN}-3.0.4-disable-analyzers.patch" )
+
+CHECKREQS_DISK_BUILD="2G"
+DOTNET_PKG_PROJECTS=( Source/BoogieDriver/BoogieDriver.csproj )
+DOTNET_PKG_BUILD_EXTRA_ARGS=( -p:RollForward=Major )
+
+pkg_setup() {
+ check-reqs_pkg_setup
+ dotnet-pkg_pkg_setup
+}
+
+src_unpack() {
+ dotnet-pkg_src_unpack
+
+ if [[ -n "${EGIT_REPO_URI}" ]] ; then
+ git-r3_src_unpack
+ fi
+}
+
+src_prepare() {
+ # Remove bad tests.
+ local -a bad_tests=(
+ civl/inductive-sequentialization/BroadcastConsensus.bpl
+ civl/inductive-sequentialization/ChangRoberts.bpl
+ civl/inductive-sequentialization/PingPong.bpl
+ civl/large-samples/GC.bpl
+ civl/paxos/is.sh
+ civl/samples/reserve.bpl
+ civl/samples/treiber-stack.bpl
+ inst/vector-generic.bpl
+ livevars/stack_overflow.bpl
+ prover/cvc5-offline.bpl
+ prover/cvc5.bpl
+ prover/exitcode.bpl
+ prover/z3-hard-timeout.bpl
+ prover/z3mutl.bpl
+ test0/AssumeFalseSplit/AssumeFalseSplit.bpl
+ test0/Split/Split.bpl
+ test15/CaptureInlineUnroll.bpl
+ test2/Timeouts0.bpl
+ test21/InterestingExamples4.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_PKG_OUTPUT}/BoogieDriver.dll'|" \
+ -i "${S}/Test/lit.site.cfg" || die "failed to update lit.site.cfg"
+
+ dotnet-pkg_src_prepare
+}
+
+src_test() {
+ einfo "Starting tests using the lit test tool."
+ local -a lit_opts=(
+ --order=lexical
+ --time-tests
+ --timeout 1800 # Let one test take no more than half a hour.
+ --verbose
+ --workers="$(makeopts_jobs)"
+ )
+ edo lit "${lit_opts[@]}" "${S}/Test"
+}
+
+src_install() {
+ dotnet-pkg-base_install
+ dotnet-pkg-base_dolauncher "/usr/share/${P}/BoogieDriver" boogie
+
+ einstalldocs
+}