Skip to content

Commit

Permalink
feat: Update dependencies and add contract annotation
Browse files Browse the repository at this point in the history
  • Loading branch information
MathieuSoysal authored Mar 5, 2024
1 parent 9863c96 commit 935463d
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 2 deletions.
2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -10,5 +10,5 @@ edition = "2021"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dev-dependencies]
[dependencies]
prusti-contracts = "0.2.0"
7 changes: 6 additions & 1 deletion src/lib.rs
Original file line number Diff line number Diff line change
@@ -1,13 +1,18 @@
#![feature(test)]
extern crate test;

use prusti_contracts::*;

const MAX_FIBONACCI: u32 = 2_971_215_073;

pub fn play_game(n: u32) {
println!("{}", fizz_buzz_fibonacci(n));

Check failure on line 9 in src/lib.rs

View workflow job for this annotation

GitHub Actions / Cargo Prusti static analysis

[Prusti: unsupported feature] unsupported constant type &'?11 [&'?12 str; Const { ty: usize, kind: Leaf(0x0000000000000002) }]

error: [Prusti: unsupported feature] unsupported constant type &'?11 [&'?12 str; Const { ty: usize, kind: Leaf(0x0000000000000002) }] --> src/lib.rs:9:14 | 9 | println!("{}", fizz_buzz_fibonacci(n)); | ^^^^
}

#[trusted]
fn is_fibonacci_number(n: u32) -> bool {
let (mut previous, mut current) = (0, 1);
while current < n && n <= 2971215073 {
while current < n && n <= MAX_FIBONACCI {
let next = previous + current;
previous = current;
current = next;
Expand Down

0 comments on commit 935463d

Please sign in to comment.