Skip to content

Commit

Permalink
Add another test
Browse files Browse the repository at this point in the history
  • Loading branch information
zhassan-aws committed Sep 19, 2024
1 parent e7dbbff commit 08134b2
Show file tree
Hide file tree
Showing 2 changed files with 35 additions and 0 deletions.
15 changes: 15 additions & 0 deletions tests/expected/llbc/basic1/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
fn test::select(@1: bool, @2: i32, @3: i32) -> i32
{
let @0: i32; // return
let @1: bool; // arg #1
let @2: i32; // arg #2
let @3: i32; // arg #3

if copy (@1) {
@0 := copy (@2)
}
else {
@0 := copy (@3)
}
return
}
20 changes: 20 additions & 0 deletions tests/expected/llbc/basic1/test.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
// 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 if condition

fn select(s: bool, x: i32, y: i32) -> i32 {
if s {
x
} else {
y
}
}


#[kani::proof]
fn main() {
let _ = select(true, 3, 7);
}

0 comments on commit 08134b2

Please sign in to comment.