Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[WIP] Various IDE improvements and new features #1334

Draft
wants to merge 90 commits into
base: master
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
90 commits
Select commit Hold shift + click to select a range
ddb4779
collecting information
cedihegi Nov 8, 2022
bbc07cc
some updates, had a lot of problems with just passing flags...
cedihegi Nov 11, 2022
dc4b1d5
passing method calls and verification items to ide
cedihegi Nov 22, 2022
dc079fa
fixed duplicate method calls
cedihegi Dec 4, 2022
c1d86d2
Fixed the issue of no_verify causing subsequent verifications to fail…
cedihegi Dec 4, 2022
207a4ad
now finding correct defpath for function calls and also handling bino…
cedihegi Dec 10, 2022
4636373
Fixed a bug for calls where the DefId can not be found apparently.
cedihegi Dec 11, 2022
e311df9
fixed minor bug and formatting
cedihegi Dec 12, 2022
3780ce1
now finding defpath's for MethodCalls too
cedihegi Dec 12, 2022
e518ef4
Figured out how to resolve MethodCalls, but we are still in trouble..
cedihegi Dec 19, 2022
295040c
Commit finally to own fork
Dec 19, 2022
7adf64e
Finally catching all relevant method calls as far as I can tell..
cedihegi Dec 29, 2022
4943255
initial quantifier instantiations working
Jan 3, 2023
0bd03b9
generating signatures correctly in some cases, struggling with traitb…
cedihegi Jan 5, 2023
fe577dc
successfully resolving projections (it seems)
cedihegi Jan 5, 2023
dedc17b
started on generating external specs for traits
cedihegi Jan 6, 2023
8812f3d
WIP: stream messages from server to client
Jan 8, 2023
c1cbde9
Managed to subst EarlyBinders
cedihegi Jan 19, 2023
b4f93ae
Merge remote-tracking branch 'upstream/master'
cedihegi Jan 19, 2023
41e1964
Merge branch 'master' into proto-extspec
cedihegi Jan 19, 2023
6facfce
upgraded my parts to current rust version
cedihegi Jan 19, 2023
3ac17ee
Asynchronously report messages from the server to the client via WebS…
Jan 31, 2023
24ad838
refactored extern spec generation to try and make it more readable.
cedihegi Feb 4, 2023
5d141eb
renamed stuff
cedihegi Feb 7, 2023
95b78ca
Merge branch 'joseph_quant' into proto-extspec
cedihegi Feb 7, 2023
9b0b5ad
Merge remote-tracking branch 'upstream/master' into proto-extspec
cedihegi Feb 7, 2023
bb6ddb2
Adjusted viper VerificationResult so we can passe times, and whether …
cedihegi Feb 8, 2023
a4dce76
WIP: restructure the process verification a bit
Feb 8, 2023
f84219c
Fixed warnings and a bug.
cedihegi Feb 8, 2023
d9e067c
renamed a file and adjusted text for IDE information output
cedihegi Feb 12, 2023
a069cef
Finish process_verification restructuring. Add a parameter for qi.pro…
Feb 12, 2023
92c92c3
Merge remote-tracking branch 'cedric/proto-extspec' into quant
Feb 12, 2023
ca86115
Changed message for fake errors and adjusted names of CompilerInfo pr…
cedihegi Feb 13, 2023
4e1a547
Merge remote-tracking branch 'jthomme1/quant' into proto-extspec
cedihegi Feb 15, 2023
26ea0af
Add QuantifierChosenTriggersMessage reporting
Feb 15, 2023
872b3c1
Merge remote-tracking branch 'cedric/proto-extspec' into quant
Feb 15, 2023
2cbc865
passing information about specifications of calls to IDE now, called …
cedihegi Feb 16, 2023
c3a2c6f
WIP: async processing of verification info
Feb 16, 2023
5ed232e
(IDE) Contract Spans are now also collected for pedges and termatinat…
cedihegi Feb 19, 2023
91b91c4
Cleaning up unused imports and debugging print statements
cedihegi Feb 19, 2023
ba54ed7
Some minor output changes
Feb 20, 2023
e4810ec
Merge cedric's branch
Feb 20, 2023
f886f8b
Minor fixes
Feb 20, 2023
93a78c7
Merge remote-tracking branch 'upstream/master' into quant
Feb 20, 2023
9ef451a
give spans of pledges to IDE and filter out trusted methods and predi…
cedihegi Feb 21, 2023
5df2a04
Merge remote-tracking branch 'joseph/quant' into proto-extspec
cedihegi Feb 21, 2023
b6ba6f6
updated ide-parts to new compiler version
cedihegi Feb 21, 2023
f27499c
Emit everything in a compiler note/message
Feb 21, 2023
cf53b8e
Make every token CamelCase
Feb 21, 2023
158b9ad
Set config variable for viper message reporting to default false.
Feb 21, 2023
195af4d
Proper camelCase messages
Feb 22, 2023
91f4ff9
Can not automatically generate extern_specs for local methods anymore
cedihegi Feb 22, 2023
82e6063
Fix GlobalRef detaching warning. Add a few comments. Remove some debu…
Feb 22, 2023
849b18d
Better comment for the VerificationRequestProcessing global variable.
Feb 22, 2023
33a2e63
Remove leftover comment.
Feb 22, 2023
ed8b1b6
Merge remote-tracking branch 'jthomme1/quant'
cedihegi Feb 22, 2023
1b1242d
Correct formatting and removed all clippy warnings except for 2
cedihegi Feb 22, 2023
ebfdd1b
Fix last 2 clippy warnings
Feb 22, 2023
ca1d9d6
Updated viper-toolchain, added various comments / documentation, addr…
cedihegi Feb 22, 2023
137f9a2
corrected tag for recent viper-ide nightly release
cedihegi Feb 22, 2023
f79e966
updated viper-toolchain again, this time to a compatible version
cedihegi Feb 23, 2023
f2fa93a
fixed error due to new scala version
cedihegi Feb 23, 2023
5600499
made testcases compile at least, but one is hard to update to new str…
cedihegi Feb 23, 2023
7e6ceaf
Fixed prusti-server test. Why do we get a 255 exit code on a successf…
Feb 23, 2023
e8bddf0
Adjusted ui testcase that has additional note about existential quant…
cedihegi Feb 23, 2023
ede8451
Bugfixes for 2 testcases. All tests should be passing now
cedihegi Feb 23, 2023
3572fea
Add debug output
Feb 24, 2023
be04342
Merge remote-tracking branch 'cedric/master' into quant
Feb 24, 2023
7d434b5
Merge remote-tracking branch 'jthomme1/quant'
cedihegi Feb 24, 2023
bac27bf
Make cache save when not using a server
Feb 25, 2023
9ca7602
Merge remote-tracking branch 'jthomme1/quant'
cedihegi Feb 25, 2023
b373c14
Gracefully close also the receiving end of the websocket.
Feb 25, 2023
e84688f
Close the websocket connection correctly
Feb 25, 2023
2cc9233
Merge remote-tracking branch 'jthomme1/quant'
cedihegi Feb 25, 2023
c39ece5
Fix bug where successful selective verification is still cached
cedihegi Feb 25, 2023
f83a088
Fix bug in translation of spans to vscode-spans
cedihegi Feb 27, 2023
8b4563f
Bump prusti version to 0.3.0
cedihegi Mar 1, 2023
eaeef45
Update viper-toolchain version
Mar 4, 2023
82b0eb8
Implement some comments (untested)
Mar 5, 2023
a492472
Fix Z3 arguments
Mar 5, 2023
f50a367
Fix test and formatting error
Mar 5, 2023
a1e6d9f
Refactor / Fix according to code reviews
cedihegi Mar 5, 2023
b144843
Format and move old comment to right location
cedihegi Mar 5, 2023
aaa3ea5
Address reviews and add comments
cedihegi Mar 5, 2023
dc6ead0
Merge remote-tracking branch 'upstream/master'
Mar 6, 2023
1f0ae07
Improve displaying of generated extern spec block for trait
cedihegi Mar 7, 2023
e562bca
Fix some quantifier reporting weirdness
Mar 7, 2023
65c99d9
Make QI etc. also work for existential quantifiers
Mar 8, 2023
a299c14
Check if current package is primary package before throwing fake_error
cedihegi Mar 9, 2023
eb05efc
Separate trait bounds from generic args and handle bad case
cedihegi Mar 13, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
WIP: restructure the process verification a bit
Joseph Thommes committed Feb 8, 2023
commit a4dce760d646c3b5247de1f2a9cf32f512fb68c0
41 changes: 0 additions & 41 deletions prusti-server/src/java_exception.rs

This file was deleted.

217 changes: 0 additions & 217 deletions prusti-server/src/jni_utils.rs

This file was deleted.

2 changes: 0 additions & 2 deletions prusti-server/src/lib.rs
Original file line number Diff line number Diff line change
@@ -11,8 +11,6 @@ mod process_verification;
mod server;
mod server_message;
mod verification_request;
mod jni_utils;
mod java_exception;

pub use client::*;
pub use process_verification::*;
Loading