autocorres: changelog+README for 1.9 release
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
parent
76ee4634e6
commit
91c135d440
|
@ -1,3 +1,8 @@
|
||||||
|
AutoCorres 1.9 (31 October 2022)
|
||||||
|
--------------
|
||||||
|
|
||||||
|
* Isabelle2021-1 edition of both AutoCorres and the C parser.
|
||||||
|
|
||||||
AutoCorres 1.8 (31 October 2021)
|
AutoCorres 1.8 (31 October 2021)
|
||||||
--------------
|
--------------
|
||||||
|
|
||||||
|
|
|
@ -32,7 +32,7 @@ AutoCorres is packaged as a theory for Isabelle2021:
|
||||||
|
|
||||||
https://isabelle.in.tum.de
|
https://isabelle.in.tum.de
|
||||||
|
|
||||||
AutoCorres currently supports three platforms: ARM, X64, and RISCV64.
|
AutoCorres currently supports four platforms: ARM, AARCH64, X64, and RISCV64.
|
||||||
The platform determines the sizes of C integral and pointer types.
|
The platform determines the sizes of C integral and pointer types.
|
||||||
|
|
||||||
For ARM, the sizes are:
|
For ARM, the sizes are:
|
||||||
|
@ -40,6 +40,11 @@ For ARM, the sizes are:
|
||||||
- 32 bits: pointers, long, int
|
- 32 bits: pointers, long, int
|
||||||
- 16 bits: short
|
- 16 bits: short
|
||||||
|
|
||||||
|
For AARCH64:
|
||||||
|
- 64 bits: pointers, long long, long
|
||||||
|
- 32 bits: int
|
||||||
|
- 16 bits: short
|
||||||
|
|
||||||
For X64:
|
For X64:
|
||||||
- 64 bits: pointers, long long, long
|
- 64 bits: pointers, long long, long
|
||||||
- 32 bits: int
|
- 32 bits: int
|
||||||
|
@ -120,9 +125,9 @@ This package contains:
|
||||||
* Compatibility word libraries and associated lemmas, for
|
* Compatibility word libraries and associated lemmas, for
|
||||||
assisting with reasoning about words (such as 32-bit words).
|
assisting with reasoning about words (such as 32-bit words).
|
||||||
|
|
||||||
* Libraries from Data61 for defining and reasoning about monads,
|
* Libraries from the l4v repository for defining and reasoning about
|
||||||
including definitions for nondeterministic state monads and option
|
monads, including definitions for nondeterministic state monads and
|
||||||
monads, along with a large proof library relating to these
|
option monads, along with a large proof library relating to these
|
||||||
definitions.
|
definitions.
|
||||||
|
|
||||||
* The "wp" weakest precondition tool, which can be used to
|
* The "wp" weakest precondition tool, which can be used to
|
||||||
|
|
Loading…
Reference in New Issue