Added missing expected file

model-checking · Dec 14, 2023 · 00bfe6e · 00bfe6e
1 parent 6192f3e
commit 00bfe6e
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 2 deletions.
diff --git a/tests/expected/function-contract/modifies/vec_pass.expected b/tests/expected/function-contract/modifies/vec_pass.expected
@@ -0,0 +1,20 @@
+modify.assertion\
+- Status: SUCCESS\
+- Description: "v.len() > 0"\
+in function modify
+
+modify_replace.assertion\
+- Status: SUCCESS\
+- Description: "element set"\
+in function modify_replace
+
+modify_replace.assertion\
+- Status: SUCCESS\
+- Description: "vector tail equality"\
+in function modify_replace
+
+assertion\
+- Status: SUCCESS\
+- Description: "v [0] == src"
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/modifies/vec_pass.rs b/tests/expected/function-contract/modifies/vec_pass.rs
@@ -9,8 +9,8 @@ fn modify(v: &mut Vec<u32>, src: u32) {
  v[0] = src
 }
 
-//#[kani::unwind(10)]
-//#[kani::proof_for_contract(modify)]
+#[kani::unwind(10)]
+#[kani::proof_for_contract(modify)]
 fn main() {
  let v_len = kani::any_where(|i| *i < 4);
  let mut v: Vec<u32> = vec![kani::any()];