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

Closed

trktby wants to merge 54 commits into

Aurel300:rewrite-2023from

trktby:rewrite-2023-assistant-features

Commits on Jun 3, 2024

Fix domain function name garbling when running over prusti-server
trktby
committed
30beba6

Commits on Jun 8, 2024

Use new VerificationResult type
trktby
committed
ec4035e

Commits on Jun 12, 2024

Change prusti-server workflow
trktby
committed
4e6cc8a

Commits on Jun 13, 2024

Port `show_ide_info` and `skip_verification` flags
trktby
committed
0849d35
Port `verify_only_defpath` and `report_viper_messages` flags
trktby
committed
5270e09

Commits on Jun 14, 2024

Add support for block level messaging and bump version
trktby
committed
39bfc55

Commits on Jun 18, 2024

Attempt to fix the only defpath flag and fix not emitting fake error
trktby
committed
99c3b2c
Port call finder
trktby
committed
e607cc0
Attempt porting QUERY_METHOD_SIGNATURE flag
trktby
committed
d472c60

Commits on Jul 5, 2024

Improve contract span emission
trktby
committed
1443c24

Commits on Jul 12, 2024

Accept defpaths argument as a single string
trktby
committed
cd45907
WIP: Restructure how verification requests are handled
trktby
committed
9f58eef
Optimize selective encoding for the non-selective case, config bug fix
trktby
committed
1de40ff

Commits on Jul 15, 2024

Use cfg_if instead of if(cfg!()) (#49)

zgrannan
authored and
trktby
committed
aaecb18
Impure Generics (#45)

zgrannan
authored and
trktby
committed
bc26f7b
Support cycles in encoders (#47)

Aurel300
authored and
trktby
committed
ca5edb3
VIR span manager, backtranslate postcondition errors

Aurel300
authored and
trktby
committed
f8527cc
add spans to statements, backtranslate precondition errors

Aurel300
authored and
trktby
committed
c513772
fix VIR translation errors

Aurel300
authored and
trktby
committed
e977267
cast tuple components in pure contexts

Aurel300
authored and
trktby
committed
0408617
update Viper toolchain, to avoid error filtering (see Silicon#735)

Aurel300
authored and
trktby
committed
9a99465
small generic fixes

Aurel300
authored and
trktby
committed
f3cf4ef
handle assertion failures, add precondition precision

Aurel300
authored and
trktby
committed
f53725a
Post-rebase fixes
trktby
committed
846c447

Commits on Jul 16, 2024

Port quantifier features skelleton from PR
trktby
committed
14025ce

Commits on Jul 18, 2024

Fix typo
trktby
committed
70b9855
Fix viper program passing and factor out cache
trktby
committed
d195424

Commits on Jul 19, 2024

Commits on Jul 20, 2024

Add back stopwatch calls
trktby
committed
1b64b36

Commits on Jul 22, 2024

Translate and emit quantifier messages
trktby
committed
a9e5021

Commits on Jul 25, 2024

Parse pos_id as usize instead of u64 in quant messages
trktby
committed
b5722f3
More server refactoring
trktby
committed
2f8c64f

Commits on Aug 1, 2024

Fix flag to use actual vectors
trktby
committed
f06740f
Move IDE related functionality to an own top-level crate
trktby
committed
9b2bf78
Move contract span collection and fix selective encoding
trktby
committed
47591c4

Commits on Aug 2, 2024

Emit entire procedure span rather than just signature in CompilerInfo
trktby
committed
ee1747c
Add viper method name backtranslation
trktby
committed
174aef5
Revert contract spans having multiple call spans
trktby
committed
b8c37ed

Commits on Aug 8, 2024

Report results per method, backtranslate block labels
trktby
committed
1ebf520

Commits on Aug 12, 2024

Merge branch 'assistant-features/request-processing-restructure' into rewrite-2023-assistant-features
trktby
committed
3e78249

Commits on Aug 15, 2024

Commits on Aug 20, 2024

Revert "small generic fixes"
trktby
committed
b708b7c
Add type parameters to pure make_generic method for consistency

erdmannc
authored and
trktby
committed
fd951ed

Commits on Aug 21, 2024

improve support for closures/quantifiers

Aurel300
authored and
trktby
committed
19de80e
Filter some block statements for range map
trktby
committed
da102cc

Commits on Aug 29, 2024

Adapt for passing through `BlockFailureMessage`s
trktby
committed
e5a323b

Commits on Aug 30, 2024

Remove most `program_name` variables from calls
trktby
committed
ef98dc6

Commits on Sep 2, 2024

Do some simplifying and add comments
trktby
committed
a614769