Alexander Stekelenburg
Alexander Stekelenburg
Yes we need support proper support for (multi-dimensional) arrays still. Treating them as pointers is incorrect since for example the following program verifies: ```c int main(void) { int a =...
I'm having a closer look at a proper encoding for arrays right now.
Thanks for the report. This is related to #1065 and #1133. As far as I know we basically don’t handle the cases where the termination checks fail. We should definitely...
> I really wasn't aware that that assumption leads to any performance issues, this is interesting. Time-wise the difference seems relatively minor (at least for small examples) but on this...
Superseded by #916
Right, so this is because `\result == p + width * y` checks if the provenance and adress of `\result` matches the provenance of `p + width * y`. This...
This looks good to me. A bunch of the errors in the CI are because the extra kernel invariant field is not filled in in the LLVM frontend (see `/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp`)...
Alright this looks good to me. However, if as you say the KernelInvariantNotEstablished error can never occur then this should probably be a SystemError, i.e. VerCors should crash if it...
Thanks for reporting this. I've hidden the "showcases" button on the website for now since these examples were quite outdated. In the future we're planning on picking a new set...
Backslash issue should be resolved with this but I can't test it since the compilation fails due to the path being to long. This happens during the generation of the...