format code

model-checking · Nov 15, 2024 · bb789a7 · bb789a7
1 parent 0937022
commit bb789a7
Show file tree

Hide file tree

Showing 6 changed files with 271 additions and 221 deletions.
diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
diff --git a/tests/expected/llbc/basic0/test.rs b/tests/expected/llbc/basic0/test.rs
@@ -12,4 +12,4 @@ fn is_zero(i: i32) -> bool {
 #[kani::proof]
 fn main() {
     let _ = is_zero(0);
-}
+}
diff --git a/tests/expected/llbc/enum_test/test.rs b/tests/expected/llbc/enum_test/test.rs
@@ -4,22 +4,18 @@
 
 //! This test checks that Kani's LLBC backend handles simple enum
 
-
 enum MyEnum {
     A(i32),
     B,
 }
 
-
 fn enum_match(e: MyEnum) -> i32 {
     match e {
-        MyEnum::A(i) => i ,
-        MyEnum::B => 0 ,
+        MyEnum::A(i) => i,
+        MyEnum::B => 0,
     }
 }
 
-
-
 #[kani::proof]
 fn main() {
     let e = MyEnum::A(1);

diff --git a/tests/expected/llbc/projection_test/test.rs b/tests/expected/llbc/projection_test/test.rs
@@ -14,19 +14,16 @@ enum MyEnum {
     B,
 }
 
-
 fn enum_match(e: MyEnum) -> i32 {
     match e {
         MyEnum::A(s, i) => s.a + i,
-        MyEnum::B => 0 ,
+        MyEnum::B => 0,
     }
 }
 
-
-
 #[kani::proof]
 fn main() {
     let s = MyStruct { a: 1, b: 2 };
-    let e = MyEnum::A(s,1);
+    let e = MyEnum::A(s, 1);
     let i = enum_match(e);
 }
diff --git a/tests/expected/llbc/struct_test/test.rs b/tests/expected/llbc/struct_test/test.rs
@@ -4,7 +4,7 @@
 
 //! This test checks that Kani's LLBC backend handles simple struct
 
-struct MyStruct{
+struct MyStruct {
     a: i32,
     b: bool,
 }

diff --git a/tests/expected/llbc/tuple_test/test.rs b/tests/expected/llbc/tuple_test/test.rs
@@ -4,7 +4,7 @@
 
 //! This test checks that Kani's LLBC backend handles simple tuple
 
-fn tuple_add (t: (i32, i32)) -> i32 {
+fn tuple_add(t: (i32, i32)) -> i32 {
     t.0 + t.1
 }