Add a test

zhassan-aws · Sep 11, 2024 · 6d46351 · 6d46351
1 parent 2b78109
commit 6d46351
Show file tree

Hide file tree

Showing 3 changed files with 56 additions and 33 deletions.
diff --git a/Cargo.lock b/Cargo.lock
@@ -220,7 +220,7 @@ dependencies = [
 
 [[package]]
 name = "build-kani"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -348,7 +348,7 @@ dependencies = [
  "heck",
  "proc-macro2 1.0.86",
  "quote 1.0.36",
- "syn 2.0.68",
+ "syn 2.0.77",
 ]
 
 [[package]]
@@ -432,7 +432,7 @@ dependencies = [
 
 [[package]]
 name = "cprover_bindings"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "lazy_static",
  "linear-map",
@@ -938,15 +938,15 @@ checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5"
 
 [[package]]
 name = "kani"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "kani_core",
  "kani_macros",
 ]
 
 [[package]]
 name = "kani-compiler"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "charon",
  "clap",
@@ -956,20 +956,22 @@ dependencies = [
  "kani_metadata",
  "lazy_static",
  "num",
+ "quote 1.0.36",
  "regex",
  "serde",
  "serde_json",
  "shell-words",
  "strum",
  "strum_macros",
+ "syn 2.0.77",
  "tracing",
  "tracing-subscriber",
  "tracing-tree 0.4.0",
 ]
 
 [[package]]
 name = "kani-driver"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -998,7 +1000,7 @@ dependencies = [
 
 [[package]]
 name = "kani-verifier"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "anyhow",
  "home",
@@ -1007,24 +1009,24 @@ dependencies = [
 
 [[package]]
 name = "kani_core"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani_macros"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
- "proc-macro-error",
+ "proc-macro-error2",
  "proc-macro2 1.0.86",
  "quote 1.0.36",
- "syn 2.0.68",
+ "syn 2.0.77",
 ]
 
 [[package]]
 name = "kani_metadata"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -1096,7 +1098,7 @@ dependencies = [
  "assert_tokens_eq",
  "proc-macro2 1.0.86",
  "quote 1.0.36",
- "syn 2.0.68",
+ "syn 2.0.77",
 ]
 
 [[package]]
@@ -1414,27 +1416,25 @@ dependencies = [
 ]
 
 [[package]]
-name = "proc-macro-error"
-version = "1.0.4"
+name = "proc-macro-error-attr2"
+version = "2.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c"
+checksum = "96de42df36bb9bba5542fe9f1a054b8cc87e172759a1868aa05c1f3acc89dfc5"
 dependencies = [
- "proc-macro-error-attr",
  "proc-macro2 1.0.86",
  "quote 1.0.36",
- "syn 1.0.109",
- "version_check",
 ]
 
 [[package]]
-name = "proc-macro-error-attr"
-version = "1.0.4"
+name = "proc-macro-error2"
+version = "2.0.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869"
+checksum = "11ec05c52be0a07b08061f7dd003e7d7092e0472bc731b4af7bb1ef876109802"
 dependencies = [
+ "proc-macro-error-attr2",
  "proc-macro2 1.0.86",
  "quote 1.0.36",
- "version_check",
+ "syn 2.0.77",
 ]
 
 [[package]]
@@ -1676,7 +1676,7 @@ dependencies = [
  "proc-macro2 1.0.86",
  "quote 1.0.36",
  "serde_derive_internals",
- "syn 2.0.68",
+ "syn 2.0.77",
 ]
 
 [[package]]
@@ -1720,7 +1720,7 @@ checksum = "500cbc0ebeb6f46627f50f3f5811ccf6bf00643be300b4c3eabc0ef55dc5b5ba"
 dependencies = [
  "proc-macro2 1.0.86",
  "quote 1.0.36",
- "syn 2.0.68",
+ "syn 2.0.77",
 ]
 
 [[package]]
@@ -1731,7 +1731,7 @@ checksum = "18d26a20a969b9e3fdf2fc2d9f21eda6c40e2de84c9408bb5d3b05d499aae711"
 dependencies = [
  "proc-macro2 1.0.86",
  "quote 1.0.36",
- "syn 2.0.68",
+ "syn 2.0.77",
 ]
 
 [[package]]
@@ -1882,7 +1882,7 @@ dependencies = [
 
 [[package]]
 name = "std"
-version = "0.54.0"
+version = "0.55.0"
 dependencies = [
  "kani",
 ]
@@ -1920,7 +1920,7 @@ dependencies = [
  "proc-macro2 1.0.86",
  "quote 1.0.36",
  "rustversion",
- "syn 2.0.68",
+ "syn 2.0.77",
 ]
 
 [[package]]
@@ -1947,9 +1947,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.68"
+version = "2.0.77"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "901fa70d88b9d6c98022e23b4136f9f3e54e4662c3bc1bd1d84a42a9a0f0c1e9"
+checksum = "9f35bcdf61fd8e7be6caf75f429fdca8beb3ed76584befb503b1569faee373ed"
 dependencies = [
  "proc-macro2 1.0.86",
  "quote 1.0.36",
@@ -2006,7 +2006,7 @@ checksum = "46c3384250002a6d5af4d114f2845d37b57521033f30d5c3f46c4d70e1197533"
 dependencies = [
  "proc-macro2 1.0.86",
  "quote 1.0.36",
- "syn 2.0.68",
+ "syn 2.0.77",
 ]
 
 [[package]]
@@ -2112,7 +2112,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
 dependencies = [
  "proc-macro2 1.0.86",
  "quote 1.0.36",
- "syn 2.0.68",
+ "syn 2.0.77",
 ]
 
 [[package]]
@@ -2497,5 +2497,5 @@ checksum = "15e934569e47891f7d9411f1a451d947a60e000ab3bd24fbb970f000387d1b3b"
 dependencies = [
  "proc-macro2 1.0.86",
  "quote 1.0.36",
- "syn 2.0.68",
+ "syn 2.0.77",
 ]
diff --git a/tests/expected/llbc/basic0/expected b/tests/expected/llbc/basic0/expected
@@ -0,0 +1,8 @@
+fn test::is_zero(@1: i32) -> bool\
+{\
+    let @0: bool; // return\
+    let @1: i32; // arg #1\
+
+    @0 := copy (@1) == const (0 : i32)\
+    return\
+}
diff --git a/tests/expected/llbc/basic0/test.rs b/tests/expected/llbc/basic0/test.rs
@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zaeneas
+
+//! This test checks that Kani's LLBC backend handles basic expressions, in this
+//! case an equality between a variable and a constant
+
+fn is_zero(i: i32) -> bool {
+    i == 0
+}
+
+#[kani::proof]
+fn main() {
+    let _ = is_zero(0);
+}