We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
specification/loops.rs
1 parent f9f8177 commit 56335dcCopy full SHA for 56335dc
tests/should_succeed/specification/loops.rs
@@ -1,6 +1,7 @@
1
extern crate creusot_contracts;
2
use creusot_contracts::*;
3
4
+#[requires(!x)]
5
pub fn while_loop_variant(x: bool) {
6
#[variant(0)]
7
while x {}
0 commit comments