Skip to content

Commit

Permalink
autocorres: README update for Isabelle2020 and RISCV64
Browse files Browse the repository at this point in the history
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
  • Loading branch information
lsf37 committed Nov 2, 2020
1 parent aff2037 commit e51ea95
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 6 deletions.
11 changes: 8 additions & 3 deletions tools/autocorres/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -35,12 +35,12 @@ Contents of this README
Installation
------------

AutoCorres is packaged as a theory for Isabelle2019:
AutoCorres is packaged as a theory for Isabelle2020:

https://isabelle.in.tum.de

AutoCorres currently supports two platforms: ARM and X64. The platform
determines the sizes of C integral and pointer types.
AutoCorres currently supports three platforms: ARM, X64, and RISCV64.
The platform determines the sizes of C integral and pointer types.

For ARM, the sizes are:
- 64 bits: long long
Expand All @@ -52,6 +52,11 @@ For X64:
- 32 bits: int
- 16 bits: short

For RISCV64:
- 64 bits: pointers, long long, long
- 32 bits: int
- 16 bits: short

To build or use AutoCorres, you must set the L4V_ARCH environment variable
according to your choice of platform.

Expand Down
11 changes: 8 additions & 3 deletions tools/autocorres/tools/release_files/README
Original file line number Diff line number Diff line change
Expand Up @@ -28,12 +28,12 @@ Contents of this README
Installation
------------

AutoCorres is packaged as a theory for Isabelle2019:
AutoCorres is packaged as a theory for Isabelle2020:

https://isabelle.in.tum.de

AutoCorres currently supports two platforms: ARM and X64. The platform
determines the sizes of C integral and pointer types.
AutoCorres currently supports three platforms: ARM, X64, and RISCV64.
The platform determines the sizes of C integral and pointer types.

For ARM, the sizes are:
- 64 bits: long long
Expand All @@ -45,6 +45,11 @@ For X64:
- 32 bits: int
- 16 bits: short

For RISCV64:
- 64 bits: pointers, long long, long
- 32 bits: int
- 16 bits: short

To build or use AutoCorres, you must set the L4V_ARCH evironment variable
according to your choice of platform.

Expand Down

0 comments on commit e51ea95

Please sign in to comment.