Gerwin Klein

Results 126 issues of Gerwin Klein

Currently `cinit lift: x_'` leaves an assumption of the form `x = t` in the assumptions, where `x` is a new parameter (the lifted `x_'`) and `x` occurs in the...

cleanup
proof tools

The `IMX8MM_EVK` platform currently does not support MCS for multicore. The combination should either be disabled in config selection or should be properly supported. Concretely the tests MULITCORE001 and MULITCORE002...

MCS
SMP
new-platform

In #877 the `TX2_*_SMP_hyp_MCS_clang_64` tests get stuck on `SCHED_CONTEXT_0014` for clang only, gcc seems to work fine. This combination is currently unsupported and disabled in the tests, but we should...

bug
MCS
SMP

See #1088 -- instead of just a syntax error we should be getting an explanation.

enhancement

See https://github.com/FasterXML/jackson-dataformats-text/issues/411 and https://github.com/FasterXML/jackson-dataformats-text/pull/412 > The IndexOutOfBoundsException is caused by a condition where the buffer is still large enough that it can hold one char, but that char is a...

bug

Should check that bazel tests work for at least different JDK LTS versions.

testing

GitHub actions have Windows runners, would be good to check that build and regression tests work there.

testing

Users should be able to provide annotations such as `@SuppressWarnings(..)` or `@Override` to the lexer function. This probably should be a new scanner directive.

enhancement

In #715 one of the features of that particular spec is a very large "or" of strings. My hypothesis there was that this tends to blow up the initial DFA...

enhancement

We can now reuse workflow definitions, which means we can factor them out into the ci-actions repo and re-use over multiple other repositories. Needs seL4/ci-actions#332 merged first. The plan is...

CI