diff --git a/tools/autocorres/README.md b/tools/autocorres/README.md index 40bd399db6..20a4c13970 100644 --- a/tools/autocorres/README.md +++ b/tools/autocorres/README.md @@ -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 @@ -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. diff --git a/tools/autocorres/tools/release_files/README b/tools/autocorres/tools/release_files/README index 23933f64fe..3ff3e85d12 100644 --- a/tools/autocorres/tools/release_files/README +++ b/tools/autocorres/tools/release_files/README @@ -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 @@ -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.