Steven Keuchel

riscv: build failure due to Werror=cast-align

2

**Describe the bug** When building for the riscv64 architecture, a build failure occurs in the test suite due to treating warnings as errors. build log snippet ``` 36.07 [ 85%]...

In the codebase we are using two kinds of environments. `Env` carries a piece of data for every element of a context, and `NamedEnv` carries data for every item in...

The heap predicates have a field that indicates which predicates are precise, and for those it splits up the arguments into inputs and outpus. https://github.com/katamaran-project/katamaran/blob/b7d951c28fc8a0ef6297b91b3531df98b7ee52f0/theories/Syntax/Predicates.v#L56-L69 I wonder why we went...

For pattern matching on unions, we have a version that allows to provide a list of alternatives. https://github.com/katamaran-project/katamaran/blob/f97ef7e664dc74c89dc3f1e19652c1d5b0f7b81a/theories/Syntax/Statements.v#L181-L182 This list is checked to be exhaustive by a type-level computation https://github.com/katamaran-project/katamaran/blob/f97ef7e664dc74c89dc3f1e19652c1d5b0f7b81a/theories/Syntax/Statements.v#L163-L167...

For the motivation see the explanation in #41. In the relational operator case in the equality check for fomulas, we start by deciding if the argument types are the same...

In our function for testing for equality of two symbolic terms of the same type, https://github.com/katamaran-project/katamaran/blob/26a30b5b62d98f76aca01c7c06611b3fe0199a6c/theories/Syntax/Terms.v#L296-L322 we throw exactly that information away in the binary op case and rather implement...

The symbolic executor uses the inductively defined symbolic propositions directly, i.e. we have essentially the two monads `□(A -> 𝕊) -> 𝕊` and `□(A -> SHeap -> 𝕊) -> SHeap...

Both the shallow and the symbolic executors are implemented in a continuation monad with a proposition answer type. Sometimes we break this abstraction. To fix this I propose to define...

The new shallow executor currently residing in `theories/Staging/NewShallow/Executor.v` uses separation logic propositions directly and does away with a shallow representation of heaps. Moreover, the soundness of this executor is proven...

The new shallow executor currently only has weak monotonicity proofs like e.g. https://github.com/katamaran-project/katamaran/blob/1ff10d9e74e66e89ed9f9729dea041f2d488d7dc/theories/Staging/NewShallow/Executor.v#L917-L922 This monotonicity property is not strong enough to finish the soundness proof of the new shallow executor....