[WIP] Various IDE improvements and new features#1334

Draft

cedihegi wants to merge 90 commits intoviperproject:masterfrom cedihegi:master

+2,390-615

Commits on Nov 8, 2022

collecting information
cedihegi
committed

Commits on Nov 11, 2022

some updates, had a lot of problems with just passing flags...
cedihegi
committed

Commits on Nov 22, 2022

passing method calls and verification items to ide
cedihegi
committed

Commits on Dec 4, 2022

fixed duplicate method calls
cedihegi
committed
Fixed the issue of no_verify causing subsequent verifications to fail by simply creating a fake error in the case
cedihegi
committed

Commits on Dec 10, 2022

now finding correct defpath for function calls and also handling binops, even though they introduce some new problems
cedihegi
committed

Commits on Dec 11, 2022

Fixed a bug for calls where the DefId can not be found apparently.
cedihegi
committed

Commits on Dec 12, 2022

Commits on Dec 19, 2022

Figured out how to resolve MethodCalls, but we are still in trouble..
cedihegi
committed
Commit finally to own fork
Joseph Thommes
committed

Commits on Dec 29, 2022

Finally catching all relevant method calls as far as I can tell..
cedihegi
committed

Commits on Jan 3, 2023

initial quantifier instantiations working
Joseph Thommes
committed

Commits on Jan 5, 2023

Commits on Jan 6, 2023

started on generating external specs for traits
cedihegi
committed

Commits on Jan 8, 2023

WIP: stream messages from server to client
Joseph Thommes
committed

Commits on Jan 31, 2023

Asynchronously report messages from the server to the client via WebSocket. Report quantifier instantiations split by methods.
Joseph Thommes
committed

Commits on Feb 4, 2023

refactored extern spec generation to try and make it more readable.
cedihegi
committed

Commits on Feb 7, 2023

Commits on Feb 8, 2023

Commits on Feb 12, 2023

Commits on Feb 13, 2023

Changed message for fake errors and adjusted names of CompilerInfo procedures.
cedihegi
committed

Commits on Feb 15, 2023

Merge remote-tracking branch 'jthomme1/quant' into proto-extspec
cedihegi
committed
Add QuantifierChosenTriggersMessage reporting
Joseph Thommes
committed
Merge remote-tracking branch 'cedric/proto-extspec' into quant
Joseph Thommes
committed

Commits on Feb 16, 2023

Commits on Feb 19, 2023

Commits on Feb 20, 2023

Some minor output changes
Joseph Thommes
committed
Merge cedric's branch
Joseph Thommes
committed
Minor fixes
Joseph Thommes
committed
Merge remote-tracking branch 'upstream/master' into quant
Joseph Thommes
committed

Commits on Feb 24, 2023

Add debug output
Joseph Thommes
committed
Merge remote-tracking branch 'cedric/master' into quant
Joseph Thommes
committed
Merge remote-tracking branch 'jthomme1/quant'
cedihegi
committed

Commits on Feb 25, 2023

Commits on Feb 27, 2023

Fix bug in translation of spans to vscode-spans
cedihegi
committed

Commits on Mar 1, 2023

Bump prusti version to 0.3.0
cedihegi
committed

Commits on Mar 4, 2023

Update viper-toolchain version
Joseph Thommes
committed

Commits on Mar 5, 2023

Implement some comments (untested)
Joseph Thommes
committed
Fix Z3 arguments
Joseph Thommes
committed
Fix test and formatting error
Joseph Thommes
committed
Refactor / Fix according to code reviews
cedihegi
committed
Format and move old comment to right location
cedihegi
committed
Address reviews and add comments
cedihegi
committed

Commits on Mar 6, 2023

Merge remote-tracking branch 'upstream/master'
Joseph Thommes
committed

Commits on Mar 7, 2023

Improve displaying of generated extern spec block for trait
cedihegi
committed
Fix some quantifier reporting weirdness
Joseph Thommes
committed

Commits on Mar 8, 2023

Make QI etc. also work for existential quantifiers
Joseph Thommes
committed

Commits on Mar 9, 2023

Check if current package is primary package before throwing fake_error
cedihegi
committed

Commits on Mar 13, 2023

Separate trait bounds from generic args and handle bad case
cedihegi
committed