Add block granularity progress indication - #262

Closed

trktby wants to merge 99 commits into

viperproject:masterfrom

trktby:quantifiers_and_selective

Commits on Oct 23, 2022

small changes
Cedric
committed
8c56c94
small fix
hegglinc
committed
9fa5ae6
invoking prusti correctly now
hegglinc
committed
6141e56

Commits on Nov 8, 2022

just slight adjustements according to changes in prusti-dev
hegglinc
committed
ef1402b

Commits on Nov 11, 2022

parsing IDE Info and passing the flag, for some reason just passing a flag is f*ing hard
hegglinc
committed
4ebe83c

Commits on Nov 21, 2022

working codelenses and codeactions
hegglinc
committed
51adf3d

Commits on Dec 4, 2022

not sure what I changed, rebase this at some point :)
hegglinc
committed
d0615eb

Commits on Dec 5, 2022

Fixing problems such as IdeInfo only saving information for one file or crate
hegglinc
committed
cfc86b5

Commits on Dec 7, 2022

IDE info is now persistent across files, i.e. when
hegglinc
committed
3984ed3

Commits on Dec 10, 2022

starting to refactor
hegglinc
committed
9dc4347

Commits on Dec 19, 2022

adjusted what happens on save, on open, etc, better behavior when collecting information but not verifying
hegglinc
committed
0d69e03

Commits on Jan 3, 2023

initial quantifier inlays working
Joseph Thommes
committed
9dc3a83

Commits on Jan 5, 2023

various changes, now able to query signatures for extern specifications
hegglinc
committed
9b3125d

Commits on Jan 9, 2023

adjusted ide-info
cedric
committed
d86e81c

Commits on Jan 31, 2023

Add hovering and splitting by function that caused the quantifier instantiations
Joseph Thommes
committed
5e7011f

Commits on Feb 5, 2023

refactoring, error handling, and some fixes
hegglinc
committed
eca362e
new snippets
hegglinc
committed
4dda223

Commits on Feb 8, 2023

Displaying checkmarks next to methods.
hegglinc
committed
dde8a60
Merge remote-tracking branch 'cedric/proto' into quant
Joseph Thommes
committed
f7fe789

Commits on Feb 11, 2023

WIP: refactored large portions and parse verification info, some bug with displaying it
hegglinc
committed
5f2aa6a
failed and successful verifications are now displayed correctly
hegglinc
committed
805c450

Commits on Feb 12, 2023

Displaying verification time and whether results were cached now works. However the textual decorators just stack in subsequent verifications so they will have to be removed at some point
cedric
committed
707bd46
Avoid parsing all messages 3 times :)
cedric
committed
e71bd1a
Add compilation and verification error differentiation. Do not show a crash message upon kill.
Joseph Thommes
committed
e9b63d9
Merge remote-tracking branch 'cedric/proto' into quant
Joseph Thommes
committed
3f707d6

Commits on Feb 13, 2023

Some formatting + documenting
cedric
committed
75fac62
Reworked underlying data structure for many features, now they all seem to be working
hegglinc
committed
df461c8
Cleaned up some unnecessary logs
hegglinc
committed
ca999e0

Commits on Feb 15, 2023

Merge remote-tracking branch 'joseph/quant' into proto
hegglinc
committed
3d37f65
fixed minor bug
hegglinc
committed
b85e0c7
Filtering fake errors out again
hegglinc
committed
104e6e5
Show QuantifierChosenTriggersMessage. Needs refactoring.
Joseph Thommes
committed
08a1b09
Merge remote-tracking branch 'cedric/proto' into quant
Joseph Thommes
committed
2a85c05

Commits on Feb 16, 2023

Now reading EncodingInfo from prusti-dev so peek feature can be used to look at specification of calls.
hegglinc
committed
aafe787
The gotoDefinition to view contracts feature is now optional
hegglinc
committed
8963526
WIP: refactor everything, not much done yet
Joseph Thommes
committed
08b5530

Commits on Feb 19, 2023

WIP: Refactoring, async reporting of results. Compiles but not at all tested.
Joseph Thommes
committed
3240872

Commits on Feb 20, 2023

minor corrections
hegglinc
committed
5eabb63

Commits on Feb 21, 2023

WIP
Joseph Thommes
committed
a907de4
resolved merge conflicts
cedric
committed
5864411
Rename compile script
Joseph Thommes
committed
3ee0009
Merge Cedric's merge!
Joseph Thommes
committed
b22e313
Change the way the output is handled.
Joseph Thommes
committed
cdde172
Make viper message showing configurable.
Joseph Thommes
committed
eda6186
Repaired Codelenses
cedric
committed
c397082
Merge remote-tracking branch 'joseph/quant' into proto
hegglinc
committed
7c28971
Gutter icons working and goto definition will show contract again
hegglinc
committed
5edac67
VerificationResults are re-rendered when changing tabs + small adjustments
hegglinc
committed
959110b

Commits on Feb 22, 2023

Changed casing. Untested, because my setup is not working
Joseph Thommes
committed
ddee515
Fixed path-problems for crates, so they are working again for
hegglinc
committed
414ba6e
Switch to camelCase everywhere. Refactor message stuff (is it better like this?). Startup prusti-server with report_viper_messages set. Other small fixes. Quantifier stuff does not yet completely w…
Joseph Thommes
committed
bd6d3e5
Remove trailing whitespaces.
Joseph Thommes
committed
4b77270

Commits on Feb 24, 2023

WIP: Make quantifiers work for crates.
Joseph Thommes
committed
abbb155

Commits on Feb 26, 2023

Make subprocess output separate, invalidate QI/QCT
Joseph Thommes
committed
1e0123a
Document methods, rename file, and improve behavior when opening files
hegglinc
committed
2882480

Commits on Feb 27, 2023

Merge remote-tracking branch 'cedric/proto' into quant
Joseph Thommes
committed
ee5e6ac

Commits on Feb 28, 2023

Check version before passing new flags and refactor / document / improve
hegglinc
committed
8739c07

Commits on Mar 1, 2023

Provide way to clear files affected by compilation
Joseph Thommes
committed
d53fbe4
Merge remote-tracking branch 'upstream/master'
hegglinc
committed
0258d4f
Resolve warnings and better naming
hegglinc
committed
f04c3bd
Remove most linter warnings
hegglinc
committed
74fe0d9
Remove linter errors and warnings, except for some unused variable warnings
hegglinc
committed
8b9365b

Commits on Mar 2, 2023

Merge remote-tracking branch 'upstream/master'
hegglinc
committed
8de5d2c
Change linter rules to allow unused arguments if starting with underscore
hegglinc
committed
ac9c2a6

Commits on Mar 4, 2023

Handle SkipVerification argument for older prusti versions
hegglinc
committed
e832a22
Bump version number to 0.12.0
Joseph Thommes
committed
9cbc2ae
Add better synchronization
Joseph Thommes
committed
07e263d
Fix linter error
Joseph Thommes
committed
86b7f21

Commits on Mar 5, 2023

Fix synchronization, explicitly add 2 env vars
Joseph Thommes
committed
367cb0d
Adjust environment variable to change in prusti-dev and small fix
cedric
committed
56350e0
Add more logging messages to find reason for failing CI
cedric
committed
8ec2df6
Debug CI by adding a timer between opening and verifying
hegglinc
committed
55fd637
Take out timeout for further debugging
hegglinc
committed
9bb29f4

Commits on Mar 6, 2023

Display a better decoration message when verification fails
hegglinc
committed
5d338da
Change text for codeLens of selective verification
hegglinc
committed
265afbf
Add the newly needed env flags to the server
Joseph Thommes
committed
7fae6eb
Another attempt to resolve the timing problems with OnOpen
hegglinc
committed
8e664a7
Merge branch 'master' of github.com:cedihegi/prusti-assistant
hegglinc
committed
9ff32e7
Fix linter errors and uninstall / remove unused library 'mutex'
hegglinc
committed
aea6a5f
New pledges and add new configuration options to README
hegglinc
committed
bcbb897

Commits on Mar 7, 2023

Improve quantifier markdown strings
Joseph Thommes
committed
2daf308
Adjust the quantifier reporting frequency
Joseph Thommes
committed
80ab5d7

Commits on Mar 8, 2023

Make the Z3 smt.qi.profile_freq configurable
Joseph Thommes
committed
4992db2

Commits on May 11, 2024

Add (incomplete) initial infrastructure for blockwise verification
trktby
committed
5107365

Commits on Jul 26, 2024

Reformat selective verification argument, add back quantifier flags
trktby
committed
51a2771

Commits on Jul 31, 2024

Fix up some flags, add extension settings, parse block messages
trktby
committed
04eec45
Display block based decorators
trktby
committed
798af9e

Commits on Aug 7, 2024

Revamp decorator management
trktby
committed
cc66a15

Commits on Aug 12, 2024

Add current block indicator, move method specific data
trktby
committed
7b0aa10
Fix current block display bug, add silicon extra arg option
trktby
committed
da37e3d

Commits on Aug 13, 2024

Compare methods by hash of trimmed string, improve decorator wiping
trktby
committed
e02e34e
Fix tab change not fetching decorators
trktby
committed
5e50d46

Commits on Aug 15, 2024

Various small fixes
trktby
committed
41a8a90

Commits on Aug 16, 2024

use setTimeout instead of setInterval
trktby
committed
22e2050
Add decorations which may or may not be used
trktby
committed
8c38340

Commits on Aug 19, 2024

Fix decorator display bugs
trktby
committed
cd46292

Commits on Aug 29, 2024

Add support for `blockFailureMessage`s
trktby
committed
4614459

Commits on Aug 30, 2024

Some cleaning
trktby
committed
9525208

Commits on Sep 16, 2024

Fix bugs
trktby
committed
9c39423