Alexander Stekelenburg

Command palete

4

I would love to see the command palete. In windows and Linux you open it with ctrl+p and on mac with ⌘⇧P

Keybinding

1

Maybe a menu for keybinding.

Update VCLLVM (now Pallas) to LLVM 17, update to newest VerCors version, and convert more instructions to COL

4

This draft PR is here to share my current progress and is not ready to be merged yet.

I think I should maybe add some more comments but this is what I have so far. For challenge 1 it's only version 0 and for challenge 2 it's only...

`refute` does not work as expected

1

According to the wiki: >VerCors also supports a refute statement, which is the opposite of assert. Internally, refute expr; is transformed into assert !(expr);, i.e. asserting the negation. Note that...

Allow the use of pointers to things that are not a reference type

7

Currently you can only take the address of a struct in the C and C++ frontends. By converting variables to pointers whenever you take their address you can do the...

Consolidating quantified field and predicate chunks

1

I noticed that state consolidation only merges basic chunks. I've been running into issues where if I have a lot of quantified field chunks things become very slow. In particular...

The following method only seems to verify if I use `--useOldAxiomatization`: ``` method lemmaUniquenessPrefix(s1: Seq[Bool], s2: Seq[Bool], prefix: Seq[Bool]) ensures (s1 == s2) == (prefix ++ s1 == prefix ++...

Minor AutoValue unsoundness

1

I just figured out a way in which AutoValue is a bit unsound if we have an abstract method like this: ```java class A { int a; int b; }...

Split Class into ByReferenceClass and ByValueClass

9

Checklist: - [ ] The wiki is updated in accordance with the changes in this PR. For example: syntax changes, semantics changes, VerCors flags changes, etc. # PR description The...