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

Report block-level verification progress, port Prusti Assistant changes #57

Draft
wants to merge 54 commits into
base: rewrite-2023
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
54 commits
Select commit Hold shift + click to select a range
30beba6
Fix domain function name garbling when running over prusti-server
trktby Jun 3, 2024
ec4035e
Use new VerificationResult type
trktby Jun 8, 2024
4e6cc8a
Change prusti-server workflow
trktby Jun 12, 2024
0849d35
Port `show_ide_info` and `skip_verification` flags
trktby Jun 13, 2024
5270e09
Port `verify_only_defpath` and `report_viper_messages` flags
trktby Jun 13, 2024
39bfc55
Add support for block level messaging and bump version
trktby Jun 14, 2024
99c3b2c
Attempt to fix the only defpath flag and fix not emitting fake error
trktby Jun 18, 2024
e607cc0
Port call finder
trktby Jun 18, 2024
d472c60
Attempt porting QUERY_METHOD_SIGNATURE flag
trktby Jun 18, 2024
1443c24
Improve contract span emission
trktby Jul 5, 2024
cd45907
Accept defpaths argument as a single string
trktby Jul 12, 2024
9f58eef
WIP: Restructure how verification requests are handled
trktby Jul 12, 2024
1de40ff
Optimize selective encoding for the non-selective case, config bug fix
trktby Jul 12, 2024
aaecb18
Use cfg_if instead of if(cfg!()) (#49)
zgrannan May 13, 2024
bc26f7b
Impure Generics (#45)
zgrannan May 14, 2024
ca5edb3
Support cycles in encoders (#47)
Aurel300 May 14, 2024
f8527cc
VIR span manager, backtranslate postcondition errors
Aurel300 Jun 18, 2024
c513772
add spans to statements, backtranslate precondition errors
Aurel300 Jun 18, 2024
e977267
fix VIR translation errors
Aurel300 Jun 22, 2024
0408617
cast tuple components in pure contexts
Aurel300 Jun 22, 2024
9a99465
update Viper toolchain, to avoid error filtering (see Silicon#735)
Aurel300 Jul 8, 2024
f3cf4ef
small generic fixes
Aurel300 Jul 8, 2024
f53725a
handle assertion failures, add precondition precision
Aurel300 Jul 8, 2024
846c447
Post-rebase fixes
trktby Jul 15, 2024
14025ce
Port quantifier features skelleton from PR
trktby Jul 16, 2024
70b9855
Fix typo
trktby Jul 18, 2024
d195424
Fix viper program passing and factor out cache
trktby Jul 18, 2024
0b30959
Fix the JVM being attempted to be instantiated multiple times
trktby Jul 19, 2024
62d2a08
Fix `GlobalRef` drop warning, change `Backend` verify signature
trktby Jul 19, 2024
9daeac6
Refactor some cache and closure handling
trktby Jul 19, 2024
c8a7399
Clean up some imports, minor other fixes
trktby Jul 19, 2024
1b64b36
Add back stopwatch calls
trktby Jul 20, 2024
a9e5021
Translate and emit quantifier messages
trktby Jul 22, 2024
b5722f3
Parse pos_id as usize instead of u64 in quant messages
trktby Jul 25, 2024
2f8c64f
More server refactoring
trktby Jul 25, 2024
f06740f
Fix flag to use actual vectors
trktby Aug 1, 2024
9b2bf78
Move IDE related functionality to an own top-level crate
trktby Aug 1, 2024
47591c4
Move contract span collection and fix selective encoding
trktby Aug 1, 2024
ee1747c
Emit entire procedure span rather than just signature in CompilerInfo
trktby Aug 2, 2024
174aef5
Add viper method name backtranslation
trktby Aug 2, 2024
b8c37ed
Revert contract spans having multiple call spans
trktby Aug 2, 2024
1ebf520
Report results per method, backtranslate block labels
trktby Aug 8, 2024
3e78249
Merge branch 'assistant-features/request-processing-restructure' into…
trktby Aug 12, 2024
81230b2
Fix error hashes colliding
trktby Aug 15, 2024
1063d9d
Filter entity messages encoded methods rather than starting with "m_"
trktby Aug 15, 2024
110e633
Fix single files not being recognized as primary package
trktby Aug 15, 2024
35fc6a1
Fix procedure identifiers not being avalable on the server process
trktby Aug 15, 2024
b708b7c
Revert "small generic fixes"
trktby Aug 20, 2024
fd951ed
Add type parameters to pure make_generic method for consistency
erdmannc Jun 5, 2024
19de80e
improve support for closures/quantifiers
Aurel300 Aug 21, 2024
da102cc
Filter some block statements for range map
trktby Aug 21, 2024
e5a323b
Adapt for passing through `BlockFailureMessage`s
trktby Aug 29, 2024
ef98dc6
Remove most `program_name` variables from calls
trktby Aug 30, 2024
a614769
Do some simplifying and add comments
trktby Aug 30, 2024
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
146 changes: 138 additions & 8 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ members = [
"viper-sys",
"vir",
"vir-proc-macro",
"ide"
]
resolver = "2"

Expand Down
Loading