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

Time reasoning #1275

Closed
wants to merge 26 commits into from
Closed

Time reasoning #1275

wants to merge 26 commits into from

Commits on Jan 25, 2023

  1. Add resource predicates 

    For now it only handles `time_credits` and `time_receipts`.
    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    cf62085 View commit details
    Browse the repository at this point in the history

  2. Add tests for time resources

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    19027ad View commit details
    Browse the repository at this point in the history

  3. Fix unfolding issue

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    72ecf6a View commit details
    Browse the repository at this point in the history

  4. Add resource predicates generation

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    76fdd0e View commit details
    Browse the repository at this point in the history

  5. Feedback

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    b674e34 View commit details
    Browse the repository at this point in the history

  6. Add flag to enable time reasoning

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    5f54d60 View commit details
    Browse the repository at this point in the history

  7. Add more test for time reasoning

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    09ef945 View commit details
    Browse the repository at this point in the history

  8. Add new tick builtin method

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    72ab443 View commit details
    Browse the repository at this point in the history

  9. Add calls to tick in loops

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    d341f99 View commit details
    Browse the repository at this point in the history

  10. Update tests

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    9366b68 View commit details
    Browse the repository at this point in the history

  11. Add more tests

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    4f9b4da View commit details
    Browse the repository at this point in the history

  12. Remove calls to tick to an exhale and an inhale for error reporting

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    dbbd4f0 View commit details
    Browse the repository at this point in the history

  13. More tests and add an expression simplifier for methods 

    Implications are brocken with time credits and receipts contraints as they
are impure but Prusti translate them into ors which viper doesn't accept.
Simplifying those expression solve this issue as they are changed back to an implication.
    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    4881b52 View commit details
    Browse the repository at this point in the history

  14. Formating

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    659b98f View commit details
    Browse the repository at this point in the history

  15. Add position to time credits/receipts expr

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    e958a4a View commit details
    Browse the repository at this point in the history

  16. Add temporary error reporting

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    c36040b View commit details
    Browse the repository at this point in the history

  17. Add more complex tests

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    5ba2c1f View commit details
    Browse the repository at this point in the history

  18. Fix position for error reporting

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    b029e94 View commit details
    Browse the repository at this point in the history

  19. Fix rebase

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    b9f2128 View commit details
    Browse the repository at this point in the history

  20. Fix clippy error

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    4267cde View commit details
    Browse the repository at this point in the history

  21. Pull request reviews

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    b85cab5 View commit details
    Browse the repository at this point in the history

  22. Add scope id to resource predicate for loop body

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    3693f84 View commit details
    Browse the repository at this point in the history

  23. Add functions to modify resource predicate scope

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    3356338 View commit details
    Browse the repository at this point in the history

  24. Add loop cost

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    4b46a5d View commit details
    Browse the repository at this point in the history

  25. More quadratic loops in a seperate test

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    0bb8266 View commit details
    Browse the repository at this point in the history

  26. Clippy

    @Pialex99
    Pialex99 committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    31c8871 View commit details
    Browse the repository at this point in the history