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

"while(i!=-1)" causes "Unsatisfied precondition constraint" #122

Closed
jyasskin opened this issue Jul 24, 2010 · 1 comment
Closed

"while(i!=-1)" causes "Unsatisfied precondition constraint" #122

jyasskin opened this issue Jul 24, 2010 · 1 comment

Comments

@jyasskin
Copy link
Contributor

$ cat ~/tmp/test.rs
fn main() {
  let int i = -1;
  while (i != -1) {
    ret;
  }
}
$ ./rustboot -L . ~/tmp/test.rs -o ~/tmp/test
~/tmp/test.rs:3:2 - 6:0:E:Error: Unsatisfied precondition constraint <init #14 = .t0> at stmt 23:
while ({
           auto .t0;
           .t0 = -1;
    }i != .t0) {
    ret;
}
$

Interestingly, changing the literal to "1" avoids the error.

@graydon
Copy link
Contributor

graydon commented Aug 24, 2010

Closed by b34cb1b.

oli-obk pushed a commit to oli-obk/rust that referenced this issue Jul 19, 2017
prevent more deallocations of statics
keeperofdakeys pushed a commit to keeperofdakeys/rust that referenced this issue Dec 12, 2017
Definitions for i686-unknown-linux-musl, arm and asmjs musl
kazcw pushed a commit to kazcw/rust that referenced this issue Oct 23, 2018
* added _mm_cvtps_pd

* added _mm_set_sd

* added _mm_set1_pd

* added _mm_set_pd1

* added _mm_set_pd

* added _mm_setr_pd

* added _mm_setzero_pd
dlrobertson pushed a commit to dlrobertson/rust that referenced this issue Nov 29, 2018
eddyb pushed a commit to eddyb/rust that referenced this issue Jun 30, 2020
bors pushed a commit to rust-lang-ci/rust that referenced this issue Oct 1, 2021
bjorn3 pushed a commit to bjorn3/rust that referenced this issue Feb 1, 2022
Rustup to rustc 1.60.0-nightly (a00e130 2022-01-29)
celinval added a commit to celinval/rust-dev that referenced this issue Nov 9, 2024
Porting from
https://github.com/model-checking/kani/blob/main/tests/expected/loop-contract/small_slice_eq.rs

The cbmc argument `--object-bits 8` is needed to avoid running out of
memory for the harness.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Celina G. Val <[email protected]>
tautschnig pushed a commit to celinval/rust-dev that referenced this issue Dec 6, 2024
)

In rust-lang#148 and rust-lang#122, we had to comment out a few harnesses due to the issue
model-checking/kani#3670. But now that the fix
has been pushed, we can enable them.
This issue was closed.
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

No branches or pull requests

2 participants