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.

Sign up for GitHub

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

Jump to bottom

New features and improvements #216

Draft
wants to merge 83 commits into
base: master
Choose a base branch
from
Draft

New features and improvements #216

wants to merge 83 commits into from

Commits on Oct 23, 2022

  1. small changes

    @cedihegi
    cedihegi committed Oct 23, 2022
    Configuration menu
    Copy the full SHA
    8c56c94 View commit details
    Browse the repository at this point in the history

  2. small fix

    @cedihegi
    cedihegi committed Oct 23, 2022
    Configuration menu
    Copy the full SHA
    9fa5ae6 View commit details
    Browse the repository at this point in the history

  3. invoking prusti correctly now

    @cedihegi
    cedihegi committed Oct 23, 2022
    Configuration menu
    Copy the full SHA
    6141e56 View commit details
    Browse the repository at this point in the history

Commits on Nov 8, 2022

  1. just slight adjustements according to changes in prusti-dev

    @cedihegi
    cedihegi committed Nov 8, 2022
    Configuration menu
    Copy the full SHA
    ef1402b View commit details
    Browse the repository at this point in the history

Commits on Nov 11, 2022

  1. parsing IDE Info and passing the flag, for some reason just passing a… 

    … flag is f*ing hard
    @cedihegi
    cedihegi committed Nov 11, 2022
    Configuration menu
    Copy the full SHA
    4ebe83c View commit details
    Browse the repository at this point in the history

Commits on Nov 21, 2022

  1. working codelenses and codeactions

    @cedihegi
    cedihegi committed Nov 21, 2022
    Configuration menu
    Copy the full SHA
    51adf3d View commit details
    Browse the repository at this point in the history

Commits on Dec 4, 2022

  1. not sure what I changed, rebase this at some point :)

    @cedihegi
    cedihegi committed Dec 4, 2022
    Configuration menu
    Copy the full SHA
    d0615eb View commit details
    Browse the repository at this point in the history

Commits on Dec 5, 2022

  1. Fixing problems such as IdeInfo only saving information for one file … 

    …or crate

and codelenses only updating after reloading a file or editing it.
    @cedihegi
    cedihegi committed Dec 5, 2022
    Configuration menu
    Copy the full SHA
    cfc86b5 View commit details
    Browse the repository at this point in the history

Commits on Dec 7, 2022

  1. IDE info is now persistent across files, i.e. when 

    verifying different files or crates, not just the info
of the most recent one is stored.
    @cedihegi
    cedihegi committed Dec 7, 2022
    Configuration menu
    Copy the full SHA
    3984ed3 View commit details
    Browse the repository at this point in the history

Commits on Dec 10, 2022

  1. starting to refactor

    @cedihegi
    cedihegi committed Dec 10, 2022
    Configuration menu
    Copy the full SHA
    9dc4347 View commit details
    Browse the repository at this point in the history

Commits on Dec 19, 2022

  1. adjusted what happens on save, on open, etc, better behavior when col… 

    …lecting information but not verifying
    @cedihegi
    cedihegi committed Dec 19, 2022
    Configuration menu
    Copy the full SHA
    0d69e03 View commit details
    Browse the repository at this point in the history

Commits on Jan 3, 2023

  1. initial quantifier inlays working

    Joseph Thommes committed Jan 3, 2023
    Configuration menu
    Copy the full SHA
    9dc3a83 View commit details
    Browse the repository at this point in the history

Commits on Jan 5, 2023

  1. various changes, now able to query signatures for extern specifications

    @cedihegi
    cedihegi committed Jan 5, 2023
    Configuration menu
    Copy the full SHA
    9b3125d View commit details
    Browse the repository at this point in the history

Commits on Jan 9, 2023

  1. adjusted ide-info

    @cedihegi
    cedihegi committed Jan 9, 2023
    Configuration menu
    Copy the full SHA
    d86e81c View commit details
    Browse the repository at this point in the history

Commits on Jan 31, 2023

  1. Add hovering and splitting by function that caused the quantifier ins… 

    …tantiations
    Joseph Thommes committed Jan 31, 2023
    Configuration menu
    Copy the full SHA
    5e7011f View commit details
    Browse the repository at this point in the history

Commits on Feb 5, 2023

  1. refactoring, error handling, and some fixes

    @cedihegi
    cedihegi committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    eca362e View commit details
    Browse the repository at this point in the history

  2. new snippets

    @cedihegi
    cedihegi committed Feb 5, 2023
    Configuration menu
    Copy the full SHA
    4dda223 View commit details
    Browse the repository at this point in the history

Commits on Feb 8, 2023

  1. Displaying checkmarks next to methods. 

    Not yet actually depending on the verification's result.
    @cedihegi
    cedihegi committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    dde8a60 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'cedric/proto' into quant

    Joseph Thommes committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    f7fe789 View commit details
    Browse the repository at this point in the history

Commits on Feb 11, 2023

  1. WIP: refactored large portions and parse verification info, some bug … 

    …with displaying it
    @cedihegi
    cedihegi committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    5f2aa6a View commit details
    Browse the repository at this point in the history

  2. failed and successful verifications are now displayed correctly

    @cedihegi
    cedihegi committed Feb 11, 2023
    Configuration menu
    Copy the full SHA
    805c450 View commit details
    Browse the repository at this point in the history

Commits on Feb 12, 2023

  1. Displaying verification time and whether results were cached now work… 

    …s. However the textual decorators just stack in subsequent verifications so they will have to be removed at some point
    @cedihegi
    cedihegi committed Feb 12, 2023
    Configuration menu
    Copy the full SHA
    707bd46 View commit details
    Browse the repository at this point in the history

  2. Avoid parsing all messages 3 times :)

    @cedihegi
    cedihegi committed Feb 12, 2023
    Configuration menu
    Copy the full SHA
    e71bd1a View commit details
    Browse the repository at this point in the history

  3. Add compilation and verification error differentiation. Do not show a… 

    … crash message upon kill.
    Joseph Thommes committed Feb 12, 2023
    Configuration menu
    Copy the full SHA
    e9b63d9 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'cedric/proto' into quant

    Joseph Thommes committed Feb 12, 2023
    Configuration menu
    Copy the full SHA
    3f707d6 View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2023

  1. Some formatting + documenting

    @cedihegi
    cedihegi committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    75fac62 View commit details
    Browse the repository at this point in the history

  2. Reworked underlying data structure for many features, now they all se… 

    …em to be working
    @cedihegi
    cedihegi committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    df461c8 View commit details
    Browse the repository at this point in the history

  3. Cleaned up some unnecessary logs

    @cedihegi
    cedihegi committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    ca999e0 View commit details
    Browse the repository at this point in the history

Commits on Feb 15, 2023

  1. Merge remote-tracking branch 'joseph/quant' into proto

    @cedihegi
    cedihegi committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    3d37f65 View commit details
    Browse the repository at this point in the history

  2. fixed minor bug

    @cedihegi
    cedihegi committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    b85e0c7 View commit details
    Browse the repository at this point in the history

  3. Filtering fake errors out again

    @cedihegi
    cedihegi committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    104e6e5 View commit details
    Browse the repository at this point in the history

  4. Show QuantifierChosenTriggersMessage. Needs refactoring.

    Joseph Thommes committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    08a1b09 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'cedric/proto' into quant

    Joseph Thommes committed Feb 15, 2023
    Configuration menu
    Copy the full SHA
    2a85c05 View commit details
    Browse the repository at this point in the history

Commits on Feb 16, 2023

  1. Now reading EncodingInfo from prusti-dev so peek feature can be used … 

    …to look at specification of calls.
    @cedihegi
    cedihegi committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    aafe787 View commit details
    Browse the repository at this point in the history

  2. The gotoDefinition to view contracts feature is now optional 

    (configurable)
    @cedihegi
    cedihegi committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    8963526 View commit details
    Browse the repository at this point in the history

  3. WIP: refactor everything, not much done yet

    Joseph Thommes committed Feb 16, 2023
    Configuration menu
    Copy the full SHA
    08b5530 View commit details
    Browse the repository at this point in the history

Commits on Feb 19, 2023

  1. WIP: Refactoring, async reporting of results. Compiles but not at all… 

    … tested.
    Joseph Thommes committed Feb 19, 2023
    Configuration menu
    Copy the full SHA
    3240872 View commit details
    Browse the repository at this point in the history

Commits on Feb 20, 2023

  1. minor corrections

    @cedihegi
    cedihegi committed Feb 20, 2023
    Configuration menu
    Copy the full SHA
    5eabb63 View commit details
    Browse the repository at this point in the history

Commits on Feb 21, 2023

  1. WIP

    Joseph Thommes committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    a907de4 View commit details
    Browse the repository at this point in the history

  2. resolved merge conflicts

    @cedihegi
    cedihegi committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    5864411 View commit details
    Browse the repository at this point in the history

  3. Rename compile script

    Joseph Thommes committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    3ee0009 View commit details
    Browse the repository at this point in the history

  4. Merge Cedric's merge!

    Joseph Thommes committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    b22e313 View commit details
    Browse the repository at this point in the history

  5. Change the way the output is handled.

    Joseph Thommes committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    cdde172 View commit details
    Browse the repository at this point in the history

  6. Make viper message showing configurable.

    Joseph Thommes committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    eda6186 View commit details
    Browse the repository at this point in the history

  7. Repaired Codelenses

    @cedihegi
    cedihegi committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    c397082 View commit details
    Browse the repository at this point in the history

  8. Merge remote-tracking branch 'joseph/quant' into proto

    @cedihegi
    cedihegi committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    7c28971 View commit details
    Browse the repository at this point in the history

  9. Gutter icons working and goto definition will show contract again

    @cedihegi
    cedihegi committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    5edac67 View commit details
    Browse the repository at this point in the history

  10. VerificationResults are re-rendered when changing tabs + small adjust… 

    …ments
    @cedihegi
    cedihegi committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    959110b View commit details
    Browse the repository at this point in the history

Commits on Feb 22, 2023

  1. Changed casing. Untested, because my setup is not working

    Joseph Thommes committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    ddee515 View commit details
    Browse the repository at this point in the history

  2. Fixed path-problems for crates, so they are working again for 

    CodeLenses, Decorators and CodeActions.
    @cedihegi
    cedihegi committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    414ba6e View commit details
    Browse the repository at this point in the history

  3. 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 work for crates or when switching tabs.
    Joseph Thommes committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    bd6d3e5 View commit details
    Browse the repository at this point in the history

  4. Remove trailing whitespaces.

    Joseph Thommes committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    4b77270 View commit details
    Browse the repository at this point in the history

Commits on Feb 24, 2023

  1. WIP: Make quantifiers work for crates.

    Joseph Thommes committed Feb 24, 2023
    Configuration menu
    Copy the full SHA
    abbb155 View commit details
    Browse the repository at this point in the history

Commits on Feb 26, 2023

  1. Make subprocess output separate, invalidate QI/QCT 

    Open a separate output window for subprocess messages to not
spam the extension output window.
Make quantifier information disappear when verifying again (but
not when skipping) and when changing the document.
Also, do not consume the output of a to-be-killed verification
that is still taking place by checking the this.runCount variable.
    Joseph Thommes committed Feb 26, 2023
    Configuration menu
    Copy the full SHA
    1e0123a View commit details
    Browse the repository at this point in the history

  2. Document methods, rename file, and improve behavior when opening files

    @cedihegi
    cedihegi committed Feb 26, 2023
    Configuration menu
    Copy the full SHA
    2882480 View commit details
    Browse the repository at this point in the history

Commits on Feb 27, 2023

  1. Merge remote-tracking branch 'cedric/proto' into quant

    Joseph Thommes committed Feb 27, 2023
    Configuration menu
    Copy the full SHA
    ee5e6ac View commit details
    Browse the repository at this point in the history

Commits on Feb 28, 2023

  1. Check version before passing new flags and refactor / document / improve 

    code
    @cedihegi
    cedihegi committed Feb 28, 2023
    Configuration menu
    Copy the full SHA
    8739c07 View commit details
    Browse the repository at this point in the history

Commits on Mar 1, 2023

  1. Provide way to clear files affected by compilation 

    It is still a bit awkward, since now the infoCollection also has
to call the verificationManager. Maybe this should change.

Moreover, now the verification arguments are wrapped in a class
to allow a cleaner passing on of them in case they are needed in
a deeper method e.g. when maybe implementing a cleaner currentRun
check or when it is needed to know whether to actually clean
something provided in an earlier run.

Also, the setting of the prusti semantic version was moved to
also affect the server correctly.

And lastly, the thresholding mechanism of the diagnostics was
changed to be more predictable.
    Joseph Thommes committed Mar 1, 2023
    Configuration menu
    Copy the full SHA
    d53fbe4 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/master'

    @cedihegi
    cedihegi committed Mar 1, 2023
    Configuration menu
    Copy the full SHA
    0258d4f View commit details
    Browse the repository at this point in the history

  3. Resolve warnings and better naming

    @cedihegi
    cedihegi committed Mar 1, 2023
    Configuration menu
    Copy the full SHA
    f04c3bd View commit details
    Browse the repository at this point in the history

  4. Remove most linter warnings

    @cedihegi
    cedihegi committed Mar 1, 2023
    Configuration menu
    Copy the full SHA
    74fe0d9 View commit details
    Browse the repository at this point in the history

  5. Remove linter errors and warnings, except for some unused variable wa… 

    …rnings
    @cedihegi
    cedihegi committed Mar 1, 2023
    Configuration menu
    Copy the full SHA
    8b9365b View commit details
    Browse the repository at this point in the history

Commits on Mar 2, 2023

  1. Merge remote-tracking branch 'upstream/master'

    @cedihegi
    cedihegi committed Mar 2, 2023
    Configuration menu
    Copy the full SHA
    8de5d2c View commit details
    Browse the repository at this point in the history

  2. Change linter rules to allow unused arguments if starting with unders… 

    …core
    @cedihegi
    cedihegi committed Mar 2, 2023
    Configuration menu
    Copy the full SHA
    ac9c2a6 View commit details
    Browse the repository at this point in the history

Commits on Mar 4, 2023

  1. Handle SkipVerification argument for older prusti versions

    @cedihegi
    cedihegi committed Mar 4, 2023
    Configuration menu
    Copy the full SHA
    e832a22 View commit details
    Browse the repository at this point in the history

  2. Bump version number to 0.12.0

    Joseph Thommes committed Mar 4, 2023
    Configuration menu
    Copy the full SHA
    9cbc2ae View commit details
    Browse the repository at this point in the history

  3. Add better synchronization

    Joseph Thommes committed Mar 4, 2023
    Configuration menu
    Copy the full SHA
    07e263d View commit details
    Browse the repository at this point in the history

  4. Fix linter error

    Joseph Thommes committed Mar 4, 2023
    Configuration menu
    Copy the full SHA
    86b7f21 View commit details
    Browse the repository at this point in the history

Commits on Mar 5, 2023

  1. Fix synchronization, explicitly add 2 env vars

    Joseph Thommes committed Mar 5, 2023
    Configuration menu
    Copy the full SHA
    367cb0d View commit details
    Browse the repository at this point in the history

  2. Adjust environment variable to change in prusti-dev and small fix

    @cedihegi
    cedihegi committed Mar 5, 2023
    Configuration menu
    Copy the full SHA
    56350e0 View commit details
    Browse the repository at this point in the history

  3. Add more logging messages to find reason for failing CI

    @cedihegi
    cedihegi committed Mar 5, 2023
    Configuration menu
    Copy the full SHA
    8ec2df6 View commit details
    Browse the repository at this point in the history

  4. Debug CI by adding a timer between opening and verifying

    @cedihegi
    cedihegi committed Mar 5, 2023
    Configuration menu
    Copy the full SHA
    55fd637 View commit details
    Browse the repository at this point in the history

  5. Take out timeout for further debugging

    @cedihegi
    cedihegi committed Mar 5, 2023
    Configuration menu
    Copy the full SHA
    9bb29f4 View commit details
    Browse the repository at this point in the history

Commits on Mar 6, 2023

  1. Display a better decoration message when verification fails

    @cedihegi
    cedihegi committed Mar 6, 2023
    Configuration menu
    Copy the full SHA
    5d338da View commit details
    Browse the repository at this point in the history

  2. Change text for codeLens of selective verification

    @cedihegi
    cedihegi committed Mar 6, 2023
    Configuration menu
    Copy the full SHA
    265afbf View commit details
    Browse the repository at this point in the history

  3. Add the newly needed env flags to the server

    Joseph Thommes committed Mar 6, 2023
    Configuration menu
    Copy the full SHA
    7fae6eb View commit details
    Browse the repository at this point in the history

  4. Another attempt to resolve the timing problems with OnOpen

    @cedihegi
    cedihegi committed Mar 6, 2023
    Configuration menu
    Copy the full SHA
    8e664a7 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' of github.com:cedihegi/prusti-assistant

    @cedihegi
    cedihegi committed Mar 6, 2023
    Configuration menu
    Copy the full SHA
    9ff32e7 View commit details
    Browse the repository at this point in the history

  6. Fix linter errors and uninstall / remove unused library 'mutex'

    @cedihegi
    cedihegi committed Mar 6, 2023
    Configuration menu
    Copy the full SHA
    aea6a5f View commit details
    Browse the repository at this point in the history

  7. New pledges and add new configuration options to README

    @cedihegi
    cedihegi committed Mar 6, 2023
    Configuration menu
    Copy the full SHA
    bcbb897 View commit details
    Browse the repository at this point in the history

Commits on Mar 7, 2023

  1. Improve quantifier markdown strings

    Joseph Thommes committed Mar 7, 2023
    Configuration menu
    Copy the full SHA
    2daf308 View commit details
    Browse the repository at this point in the history

  2. Adjust the quantifier reporting frequency

    Joseph Thommes committed Mar 7, 2023
    Configuration menu
    Copy the full SHA
    80ab5d7 View commit details
    Browse the repository at this point in the history

Commits on Mar 8, 2023

  1. Make the Z3 smt.qi.profile_freq configurable

    Joseph Thommes committed Mar 8, 2023
    Configuration menu
    Copy the full SHA
    4992db2 View commit details
    Browse the repository at this point in the history