Your message dated Fri, 22 Nov 2024 19:00:48 +0000
with message-id <e1teytc-003kzs...@fasolo.debian.org>
and subject line Bug#1067819: fixed in linksem 0.8+dfsg3-1
has caused the Debian Bug report #1067819,
regarding ITP: linksem -- Semantic model for aspects of ELF static linking and
DWARF debug information
to be marked as done.
This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.
(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact ow...@bugs.debian.org
immediately.)
--
1067819: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1067819
Debian Bug Tracking System
Contact ow...@bugs.debian.org with problems
--- Begin Message ---
Package: wnpp
Severity: wishlist
Owner: Bo YU <tsu.y...@gmail.com>
X-Debbugs-Cc: debian-de...@lists.debian.org,
debian-ocaml-ma...@lists.debian.org
* Package name : linksem
Version : 0.8
Upstream Contact: Linksem Devs <cl-linksem-...@lists.cam.ac.uk>
* URL : https://github.com/rems-project/linksem
* License : BSD-2
Programming Lang: OCaml
Description : Semantic model for aspects of ELF static linking and DWARF
debug information
Linksem is a formalisation of substantial parts of ELF linking and DWARF debug
information. It contains:
A formalisation of the core ELF file format, the de facto standard executable
and linkable file format on Linux and related systems, written in Lem. This
formalisation has been tested against approximately 5,000 ELF binaries found
"in the wild" on various different platforms.
A partial formalisation of various aspects of the platform Application Binary
Interfaces for AMD64, Power64, AArch64, and X86-32, as well as a partial
formalisation of the GNU extensions for ELF that the Linux operating system
expects. These formalisations have been formalised on an ad hoc basis, as they
were needed and may (almost certainly will be) incomplete.
An executable linker/link-checker built atop the aforementioned ELF and ABI
formalisations for AMD64, capable of linking complex link-jobs such as bzip2,
derived from an OCaml extraction of the Lem models above.
A sample proof of correctness for AMD64 relocation, using an Isabelle/HOL
extraction of the linker, ELF model, and ABI formalisations mentioned above.
A formalisation of the DWARF debug information format, as an executable
specification that interprets the DWARF information.
The ELF formalisation (and parts of the ABI formalisation) are currently also
being used as a subcomponent of the rmem architectural exploration tool, for
parsing ELF files and setting up initial machine states.
---------->------------
This is a critical dependency for sail[0]. But it depends on lem[1] first.
[0]: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1065419
[1]: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1065658
--
Regards,
--
Bo YU
signature.asc
Description: PGP signature
--- End Message ---
--- Begin Message ---
Source: linksem
Source-Version: 0.8+dfsg3-1
Done: Bo YU <tsu.y...@gmail.com>
We believe that the bug you reported is fixed in the latest version of
linksem, which is due to be installed in the Debian FTP archive.
A summary of the changes between this version and the previous one is
attached.
Thank you for reporting the bug, which will now be closed. If you
have further comments please address them to 1067...@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Bo YU <tsu.y...@gmail.com> (supplier of updated linksem package)
(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmas...@ftp-master.debian.org)
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256
Format: 1.8
Date: Wed, 09 Oct 2024 22:50:41 +0800
Source: linksem
Binary: liblinksem-ocaml-dev
Architecture: source amd64
Version: 0.8+dfsg3-1
Distribution: unstable
Urgency: low
Maintainer: Debian OCaml Maintainers <debian-ocaml-ma...@lists.debian.org>
Changed-By: Bo YU <tsu.y...@gmail.com>
Description:
liblinksem-ocaml-dev - Formalisation of the core ELF and DWARF file formats
written in L
Closes: 1067819
Changes:
linksem (0.8+dfsg3-1) unstable; urgency=low
.
* Initial release. (Closes: #1067819)
Checksums-Sha1:
5d969d71cd9b2584c1ded036242c4d8c346f5c3d 2057 linksem_0.8+dfsg3-1.dsc
0d57d104287cb37e1950f470c3502b85596af367 487052 linksem_0.8+dfsg3.orig.tar.xz
5fb0e7f02e4004edc3f4d86779fcfeded57bee7b 4564 linksem_0.8+dfsg3-1.debian.tar.xz
89ebed6f460efd74b3fd061613dbd582a9e95579 15707352
liblinksem-ocaml-dev_0.8+dfsg3-1_amd64.deb
b482e042f79e17c4c386810a0179480a3a1f8a04 6508
linksem_0.8+dfsg3-1_amd64.buildinfo
Checksums-Sha256:
570949dd08f558415d474f8009bff47dda520b0b092b1cc3395b9933a82a8d3e 2057
linksem_0.8+dfsg3-1.dsc
a61f40a9994299c6834a77b5c6f0180643d32b0658a107fbba43332f34079814 487052
linksem_0.8+dfsg3.orig.tar.xz
e87bb5916b9d56b2d18245a20cafb46af2809776c529526c7c0f2adabd150d30 4564
linksem_0.8+dfsg3-1.debian.tar.xz
4bca0ac67abb1a7dea7c3e79f6d2830bed254b9967d7b70a5b8afb5dc66bab02 15707352
liblinksem-ocaml-dev_0.8+dfsg3-1_amd64.deb
5a98e43c40a6fe2518eb7e0a380c04d1fc12ad37b3699729130f8991f1ad15b9 6508
linksem_0.8+dfsg3-1_amd64.buildinfo
Files:
7d72290fffce46f0f3df600960498b65 2057 ocaml optional linksem_0.8+dfsg3-1.dsc
984fd25c07b56e89193adde3a69c3a49 487052 ocaml optional
linksem_0.8+dfsg3.orig.tar.xz
31881337d2fc03f977e38c73ac7cbf48 4564 ocaml optional
linksem_0.8+dfsg3-1.debian.tar.xz
c988b0ddd9f8198e8407265099176fb9 15707352 ocaml optional
liblinksem-ocaml-dev_0.8+dfsg3-1_amd64.deb
c52dfd0e9233a180ff1e82dc6b35ebc2 6508 ocaml optional
linksem_0.8+dfsg3-1_amd64.buildinfo
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCAAdFiEEkpeKbhleSSGCX3/w808JdE6fXdkFAmdAcRwACgkQ808JdE6f
XdmljQ//V9L+AHapPBjdUggXO9Y29TNvhPwsZhBZ+ZvuZ2MOw2GepEPA0LnpV9c5
MMI4sm9fazcfbJOKBtc3jHuMye0tuAE38mtq5cqV/FxMotnq3hdLtv38hXd3aBKY
JIqgfUwch4YBKh3yM8irNoVPN2yzz8UOY+FTC5IcC54nJ8goM+OHX+pQX2gUh4lz
Yjge62R4CiXbrGUQfpQTzHd7UrcdBs2hkjUH33LUgtjiz5yGNTRMBRtQj6KxSWIx
bzZdbO9wAsnaBcMXDoyMoJ+LuJ05sRXTP731i0lQmTE47f3hxKOuVH1sydN7RSSL
L5GBrkIO1P9y1aYdgeIXm/DjKm5X247lmgnSNjo6dse9BEzlAcydDKH2UpYG4ku9
LslTUdu3vUt8V2EGQJx87H6JXqoScCyljZQjD7/Vg0zFpItNEBI8iGEy46LTmLv8
htHUU8jlUjcvRFWCP6c64rJKpsvSrDtF1a0lULtFqiA/GTowmdqLUSV3kOWF4M0e
ajWE+iLVWIRHEAbuNEgDR1whMu/Mt8SP42+tP5gJPDBN3r60p0Q9LMGuP0SpeG9M
5wSmJUE/mNj3KmzdEg4wEJxemhHvAO46Mygw9doFy3ma8MLiNjKUZ+PHsRCD+cr8
OpbZiUTRKKYW5RwgGbyN6x1Y69Hsyj+tuMc9v6HNpg9sX0LDj8s=
=uUfx
-----END PGP SIGNATURE-----
pgpg2mpuYHxU_.pgp
Description: PGP signature
--- End Message ---
