fix(prusti): Add #[trusted] attribute to play_game functions

MathieuSoysal · Mar 5, 2024 · ddc9f72 · ddc9f72
1 parent 935463d
commit ddc9f72
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/src/lib.rs b/src/lib.rs
@@ -5,6 +5,7 @@ use prusti_contracts::*;
 
 const MAX_FIBONACCI: u32 = 2_971_215_073;
 
+#[trusted]
 pub fn play_game(n: u32) {
     println!("{}", fizz_buzz_fibonacci(n));
 }

diff --git a/src/main.rs b/src/main.rs
@@ -1,8 +1,11 @@
 #![feature(test)]
 extern crate test;
 
+use prusti_contracts::*;
+
 use template_exercisme::play_game;
 
+#[trusted]
 fn main() {
     let args: Vec<String> = std::env::args().collect();
     let i = args