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

Add TimSort rewritten code #932

Open
wants to merge 17 commits into
base: master
Choose a base branch
from

Conversation

Omar0Tarek
Copy link

rewriting TimSort implementation code to be ready for verification

@vakaras
Copy link
Contributor

vakaras commented Mar 29, 2022

Add /home/data/eth/rust/prusti-dev2/prusti-tests/tests/cargotest.rs:

#[cargo_test]
fn test_timsort() {
    test_local_project("verifying_tim_sort");
}

@fpoli
Copy link
Member

fpoli commented Mar 29, 2022

Is the temp file there by mistake?

@Omar0Tarek Omar0Tarek changed the title add TimSort rewritten code Add TimSort rewritten code Mar 29, 2022
@@ -0,0 +1,57 @@
extern crate prusti_contracts;
use prusti_contracts::*;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please remove this file.

@vakaras
Copy link
Contributor

vakaras commented Mar 29, 2022

@Omar0Tarek Please fix the errors so that the CI passes. You should be able to run the test locally as follows:

./x.py build --all; ./x.py test timsort

P. S. You need to run ./x.py setup if you have not done that already.

@Omar0Tarek
Copy link
Author

Omar0Tarek commented Apr 22, 2022

I finished verifying the absence of panics and overflows.

When I run Prusti from the IDE, the verification succeeds, but when I run the CI tests locally, they fail producing the following error.

error: [Prusti internal error] Prusti encountered an unexpected internal error
  |
  = help: This could be caused by too small assertion timeout. Try increasing it by setting the configuration parameter ASSERT_TIMEOUT to a larger value.
  = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: Details: unregistered verification error: [application.precondition:insufficient.permission; 0] Precondition of function snap$__$TY$__Snap$Slice$i32$ might not hold. There might be insufficient permission to access Slice$i32(_1.val_ref) (@0.0)

error: could not compile `verifying_tim_sort` due to previous error; 62 warnings emitted
', prusti-tests/tests/cargotest.rs:177:18
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

@vakaras
Copy link
Contributor

vakaras commented Apr 22, 2022

I finished verifying the absence of panics and overflows.

When I run Prusti from the IDE, the verification succeeds, but when I run the CI tests locally, they fail producing the following error.

error: [Prusti internal error] Prusti encountered an unexpected internal error
  |
  = help: This could be caused by too small assertion timeout. Try increasing it by setting the configuration parameter ASSERT_TIMEOUT to a larger value.
  = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: Details: unregistered verification error: [application.precondition:insufficient.permission; 0] Precondition of function snap$__$TY$__Snap$Slice$i32$ might not hold. There might be insufficient permission to access Slice$i32(_1.val_ref) (@0.0)

error: could not compile `verifying_tim_sort` due to previous error; 62 warnings emitted
', prusti-tests/tests/cargotest.rs:177:18
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

I think this is caused by the example being very large and stressing the limits of the verifier. Since the example verifies on CI, it seems to be fine.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants