Platform constants were previously not translated. When they were moved
to translated code, some constructor issues came up.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
The names for `kernelBase` and `physBase` are renamed to `pptrBase` and
`paddrBase` respectively to be more consistent with the C (and the
previous commit).
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This update reflects a set of changes made to the seL4 kernel some time
ago that consolidates the definitions for physical to virtual
translation.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Remove resolve_address_bits'.simps from the simp set at the definition
site, instead of in the middle of the proofs.
Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>
The file was not included anywhere so far and is referenced in ML_Goal,
which is part of the AutoCorres release (but the dependency
ML_Goal_Test will be missed if it's not included elsewhere).
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
In Isabelle2020, when isabelle jedit is started without a session
context, e.g. `isabelle jedit -l ASpec`, theory imports with path
references cause the isabelle process to hang.
Since sessions now declare directories, Isabelle can find those files
without path reference and we therefore remove all such path references
from import statements. With this, `jedit` and `build` should work with
and without explicit session context as before.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
Make these a separate target so that other sessions that depend on
ASpec can kick off generation of these files (necessary because some
are mentioned in spec/ROOT, and the session structure will fail if they
don't exist).
This is only relevant in a fresh check-out when you've never built
ASpec, but in test environments this can happen if only specific
sessions are tested.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit ignores the Isabelle version set in the repo manifest and fixes
Isabelle2020 instead for github CI checks. The main purpose is to test this
function and to make sure the test can remain working while the repo manifest
is being updated.
After that has happened, this commit can be reverted.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This should not be ignored longer term. The test itself is failing anyway,
but the code now throws an exception, which it shouldn't do.
See VER-1295
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
SimplExportAndRefine is now split into two steps;
AutoCorresTest moved to its own directory.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
Rafal Kolanski
Curtis Millar
Gerwin Klein
Corey Lewis
Gerwin Klein