Add a guide for how to write commit messages and commit message tags to
make the messages more consistent and to help new people on the project
get started more quickly.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- add ghost state corresponding to gsPTTypes in Haskell and ASpec
- add ghost type comments
- style update for old definitions since we need to touch most of these
- define vs/pt_array_len for use in C annotations
- make NormalPT_T/VSRootPT_T names available for use in C annotations
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This gets rid of the simplified warning for Collect_const that
ccorres_rewrite produces in many CRefine proofs.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Contexts have the "visible" flag that determine whether warnings such
as duplicate rewrite rules are shown or not. Make setting this flag to
false available in Eisbach methods.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
If we don't provide the additional name fragment, previous artifacts
would be overwritten, which leads to a failure with error message on
GitHub.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This will now test with the following num_domains settings:
- PRs: default as in config file, no matrix
- push to master: with NUM_DOMAINS = 1 and default (= '')
- weekly test: with NUM_DOMAINS = 1, 7, and default
The default in the current config files is 16. 1 leads to structural
code changes is the setting most likely to break. 7 is for checking
that the proofs also work with a value that is not a power of 2.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Setting the environment variable INPUT_NUM_DOMAINS will cause the
build to override the KernelNumDomains setting in the config file with
the provided setting.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This adds information about the return relation to the C guards
and the C preconditions of the assumptions.
The C hoare triples for cond have also been consolidated, to
help simplify applications where the C guards are minimal.
A comment about its intended use is given.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Length argument for these functions was previously unsigned int, which
was fine for AArch32, but an implicit downcast on AArch64. Changing it
to word_t makes it unsigned long, thus requiring signature update in
ccorres proofs.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
AutoCorres no longer depends on the Lib session. This means:
- remove Lib session ROOT parsing in release.py
- copy over ROOT files of new library sessions
- add new theory NatBitWise to manifest
- update release ROOTS and ROOT files
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Achim D. Brucker
Gerwin Klein
Michael McInerney
Rafal Kolanski