diff --git a/scripts/cbmc_json_parser.py b/scripts/cbmc_json_parser.py index 9a0d58387f04..f0c0d1537d64 100755 --- a/scripts/cbmc_json_parser.py +++ b/scripts/cbmc_json_parser.py @@ -203,6 +203,7 @@ def postprocess_results(properties): has_failed_unwinding_asserts = has_check_failure(properties, GlobalMessages.UNWINDING_ASSERT_DESC) properties, reach_checks = filter_reach_checks(properties) annotate_properties_with_reach_results(properties, reach_checks) + remove_check_ids_from_description(properties) for property in properties: if has_reachable_unsupported_constructs or has_failed_unwinding_asserts: @@ -283,9 +284,6 @@ def annotate_properties_with_reach_results(properties, reach_checks): prop = get_matching_property(properties, check_id) # Attach the result of the reachability check to this property prop[GlobalMessages.REACH_CHECK_KEY] = reach_check["status"] - # Remove the ID from the property's description so that it's not shown - # to the user - prop["description"] = prop["description"].replace("[" + check_id + "] ", "", 1) def get_matching_property(properties, check_id): @@ -298,6 +296,26 @@ def get_matching_property(properties, check_id): raise Exception("Error: failed to find a property with ID \"" + check_id + "\"") +def remove_check_ids_from_description(properties): + """ + Some asserts generated by Kani have a unique ID in their description that is + of the form: + + [KANI_CHECK_ID__] + + e.g.: + + [KANI_CHECK_ID_foo.6875c808::foo_0] assertion failed: x % 2 == 0 + + This function removes those IDs from the property's description so that + they're not shown to the user. The removal of the IDs should only be done + after all ID-based post-processing is done. + """ + check_id_pattern = re.compile(r"\[" + GlobalMessages.CHECK_ID + r"_.*_[0-9]*\] ") + for property in properties: + property["description"] = re.sub(check_id_pattern, "", property["description"]) + + def construct_solver_information_message(solver_information): """ From the extracted information, construct a message and append to the final Output diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 822576a39683..959bd5f6155e 100644 --- a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -5,6 +5,7 @@ use super::typ::FN_RETURN_VOID_VAR_NAME; use crate::codegen_cprover_gotoc::utils; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type}; +use kani_queries::UserInput; use rustc_hir::def_id::DefId; use rustc_middle::mir; use rustc_middle::mir::{ @@ -89,15 +90,27 @@ impl<'tcx> GotocCtx<'tcx> { msg.description() }; + // TODO: switch to tagging assertions via the property class once CBMC allows that: + // https://github.com/diffblue/cbmc/issues/6692 + let (msg_str, reach_stmt) = if self.queries.get_check_assertion_reachability() { + let check_id = self.next_check_id(); + let msg_str = GotocCtx::add_prefix_to_msg(msg, &check_id); + let reach_msg = GotocCtx::reachability_check_message(&check_id); + (msg_str, self.codegen_cover_loc(&reach_msg, Some(term.source_info.span))) + } else { + (msg.to_string(), Stmt::skip(loc)) + }; + Stmt::block( vec![ + reach_stmt, cond.cast_to(Type::bool()).if_then_else( - Stmt::goto(self.current_fn().find_label(target), loc.clone()), + Stmt::goto(self.current_fn().find_label(target), loc), None, - loc.clone(), + loc, ), - Stmt::assert_false(msg, loc.clone()), - Stmt::goto(self.current_fn().find_label(target), loc.clone()), + Stmt::assert_false(&msg_str, loc), + Stmt::goto(self.current_fn().find_label(target), loc), ], loc, ) diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/src/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 7e5ebdff24de..6951b415cda1 100644 --- a/src/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/src/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -165,34 +165,38 @@ impl<'tcx> GotocHook<'tcx> for Assert { assert_eq!(fargs.len(), 2); let cond = fargs.remove(0).cast_to(Type::bool()); let msg = fargs.remove(0); - let mut msg = utils::extract_const_message(&msg).unwrap(); + let msg = utils::extract_const_message(&msg).unwrap(); let target = target.unwrap(); let caller_loc = tcx.codegen_caller_span(&span); - let mut stmts: Vec = Vec::new(); - - if tcx.queries.get_check_assertion_reachability() { + // TODO: switch to tagging assertions via the property class once CBMC allows that: + // https://github.com/diffblue/cbmc/issues/6692 + let (msg, reach_stmt) = if tcx.queries.get_check_assertion_reachability() { // Generate a unique ID for the assert let assert_id = tcx.next_check_id(); - // Use a description of the form: - // [KANI_REACHABILITY_CHECK] - // for reachability checks - msg = format!("[{}] {}", assert_id, msg); - let reach_msg = format!("[KANI_REACHABILITY_CHECK] {}", assert_id); + // Add this ID as a prefix to the assert message so that it can be + // easily paired with the reachability check + let msg = GotocCtx::add_prefix_to_msg(&msg, &assert_id); + let reach_msg = GotocCtx::reachability_check_message(&assert_id); // inject a reachability (cover) check to the current location - stmts.push(tcx.codegen_cover_loc(&reach_msg, span)); - } + (msg, tcx.codegen_cover_loc(&reach_msg, span)) + } else { + (msg, Stmt::skip(caller_loc)) + }; // Since `cond` might have side effects, assign it to a temporary // variable so that it's evaluated once, then assert and assume it let tmp = tcx.gen_temp_variable(cond.typ().clone(), caller_loc.clone()).to_expr(); - stmts.append(&mut vec![ - Stmt::decl(tmp.clone(), Some(cond), caller_loc.clone()), - Stmt::assert(tmp.clone(), &msg, caller_loc.clone()), - Stmt::assume(tmp, caller_loc.clone()), - Stmt::goto(tcx.current_fn().find_label(&target), caller_loc.clone()), - ]); - Stmt::block(stmts, caller_loc) + Stmt::block( + vec![ + reach_stmt, + Stmt::decl(tmp.clone(), Some(cond), caller_loc.clone()), + Stmt::assert(tmp.clone(), &msg, caller_loc.clone()), + Stmt::assume(tmp, caller_loc.clone()), + Stmt::goto(tcx.current_fn().find_label(&target), caller_loc.clone()), + ], + caller_loc, + ) } } diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/src/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index 956f34c44283..ff552627a194 100644 --- a/src/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/src/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -109,6 +109,22 @@ impl<'tcx> GotocCtx<'tcx> { // TODO: use def_id https://github.com/model-checking/kani/issues/364 idx.to_string().into() } + + /// Add a prefix of the form: + /// [] + /// to the provided message + pub fn add_prefix_to_msg(msg: &str, prefix: &str) -> String { + format!("[{}] {}", prefix, msg) + } + + /// Generate a message for the reachability check of an assert with ID + /// `check_id`. The message is of the form: + /// [KANI_REACHABILITY_CHECK] + /// The check_id is generated using the GotocCtx::next_check_id method and + /// is a unique string identifier for that check. + pub fn reachability_check_message(check_id: &str) -> String { + format!("[KANI_REACHABILITY_CHECK] {}", check_id) + } } /// The full crate name should use the Codegen Unit builder to include full name resolution, diff --git a/tests/expected/reach/bounds/reachable_fail/expected b/tests/expected/reach/bounds/reachable_fail/expected new file mode 100644 index 000000000000..af85e2d95ac4 --- /dev/null +++ b/tests/expected/reach/bounds/reachable_fail/expected @@ -0,0 +1,2 @@ +FAILURE +Failed Checks: index out of bounds: the length is less than or equal to the given index diff --git a/tests/expected/reach/bounds/reachable_fail/test.rs b/tests/expected/reach/bounds/reachable_fail/test.rs new file mode 100644 index 000000000000..05953e202502 --- /dev/null +++ b/tests/expected/reach/bounds/reachable_fail/test.rs @@ -0,0 +1,16 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks + +// This test checks that kani injects a reachability check for +// index-out-of-bounds checks and that it reports ones that are unreachable. +// The check in this test is reachable and doesn't hold, so should be reported +// as FAILURE + +fn get(s: &[i16], index: usize) -> i16 { + s[index] +} + +fn main() { + get(&[7, -83, 19], 15); +} diff --git a/tests/expected/reach/bounds/reachable_pass/expected b/tests/expected/reach/bounds/reachable_pass/expected new file mode 100644 index 000000000000..ff43ca409150 --- /dev/null +++ b/tests/expected/reach/bounds/reachable_pass/expected @@ -0,0 +1 @@ +SUCCESS diff --git a/tests/expected/reach/bounds/reachable_pass/test.rs b/tests/expected/reach/bounds/reachable_pass/test.rs new file mode 100644 index 000000000000..fdf49d14e546 --- /dev/null +++ b/tests/expected/reach/bounds/reachable_pass/test.rs @@ -0,0 +1,15 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks + +// This test checks that kani injects a reachability check for +// index-out-of-bounds checks and that it reports ones that are unreachable. +// The check in this test is reachable, so should be reported as SUCCESS + +fn get(s: &[i16], index: usize) -> i16 { + if index < s.len() { s[index] } else { -1 } +} + +fn main() { + get(&[7, -83, 19], 2); +} diff --git a/tests/expected/reach/bounds/unreachable/expected b/tests/expected/reach/bounds/unreachable/expected new file mode 100644 index 000000000000..7703d171eb67 --- /dev/null +++ b/tests/expected/reach/bounds/unreachable/expected @@ -0,0 +1 @@ +UNREACHABLE diff --git a/tests/expected/reach/bounds/unreachable/test.rs b/tests/expected/reach/bounds/unreachable/test.rs new file mode 100644 index 000000000000..f4b420d7d6f8 --- /dev/null +++ b/tests/expected/reach/bounds/unreachable/test.rs @@ -0,0 +1,16 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks + +// This test checks that kani injects a reachability check for +// index-out-of-bounds checks and that it reports ones that are unreachable. +// The check in this test is unreachable, so should be reported as UNREACHABLE + +fn get(s: &[i16], index: usize) -> i16 { + if index < s.len() { s[index] } else { -1 } +} + +fn main() { + //get(&[7, -83, 19], 2); + get(&[5, 206, -46, 321, 8], 8); +} diff --git a/tests/expected/reach/div-zero/reachable_fail/expected b/tests/expected/reach/div-zero/reachable_fail/expected new file mode 100644 index 000000000000..f7ed46aa97ba --- /dev/null +++ b/tests/expected/reach/div-zero/reachable_fail/expected @@ -0,0 +1,2 @@ +FAILURE +Failed Checks: attempt to divide by zero diff --git a/tests/expected/reach/div-zero/reachable_fail/test.rs b/tests/expected/reach/div-zero/reachable_fail/test.rs new file mode 100644 index 000000000000..000abd686c6b --- /dev/null +++ b/tests/expected/reach/div-zero/reachable_fail/test.rs @@ -0,0 +1,16 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks + +// This test checks that kani injects a reachability check for +// divide-by-zero checks and that it reports ones that are unreachable. +// The check in this test is reachable and doesn't hold, so should be reported +// as FAILURE + +fn div(x: u16, y: u16) -> u16 { + x / y +} + +fn main() { + div(678, 0); +} diff --git a/tests/expected/reach/div-zero/reachable_pass/expected b/tests/expected/reach/div-zero/reachable_pass/expected new file mode 100644 index 000000000000..ff43ca409150 --- /dev/null +++ b/tests/expected/reach/div-zero/reachable_pass/expected @@ -0,0 +1 @@ +SUCCESS diff --git a/tests/expected/reach/div-zero/reachable_pass/test.rs b/tests/expected/reach/div-zero/reachable_pass/test.rs new file mode 100644 index 000000000000..d1ad72adddd1 --- /dev/null +++ b/tests/expected/reach/div-zero/reachable_pass/test.rs @@ -0,0 +1,15 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks + +// This test checks that kani injects a reachability check for +// divide-by-zero checks and that it reports ones that are unreachable. +// The check in this test is reachable, so should be reported as SUCCESS + +fn div(x: u16, y: u16) -> u16 { + if y != 0 { x / y } else { 0 } +} + +fn main() { + div(11, 3); +} diff --git a/tests/expected/reach/div-zero/unreachable/expected b/tests/expected/reach/div-zero/unreachable/expected new file mode 100644 index 000000000000..7703d171eb67 --- /dev/null +++ b/tests/expected/reach/div-zero/unreachable/expected @@ -0,0 +1 @@ +UNREACHABLE diff --git a/tests/expected/reach/div-zero/unreachable/test.rs b/tests/expected/reach/div-zero/unreachable/test.rs new file mode 100644 index 000000000000..1a01b2f36631 --- /dev/null +++ b/tests/expected/reach/div-zero/unreachable/test.rs @@ -0,0 +1,15 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks + +// This test checks that kani injects a reachability check for +// divide-by-zero checks and that it reports ones that are unreachable. +// The check in this test is unreachable, so should be reported as UNREACHABLE + +fn div(x: u16, y: u16) -> u16 { + if y != 0 { x / y } else { 0 } +} + +fn main() { + div(5, 0); +} diff --git a/tests/expected/reach/overflow-neg/reachable_fail/expected b/tests/expected/reach/overflow-neg/reachable_fail/expected new file mode 100644 index 000000000000..9306b970b0c4 --- /dev/null +++ b/tests/expected/reach/overflow-neg/reachable_fail/expected @@ -0,0 +1,2 @@ +FAILURE +Failed Checks: attempt to negate with overflow diff --git a/tests/expected/reach/overflow-neg/reachable_fail/test.rs b/tests/expected/reach/overflow-neg/reachable_fail/test.rs new file mode 100644 index 000000000000..e67efaf81893 --- /dev/null +++ b/tests/expected/reach/overflow-neg/reachable_fail/test.rs @@ -0,0 +1,16 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular + +// This test checks that kani injects a reachability check for negation +// overflow checks and that it reports ones that are unreachable +// The negation overflow check in this test is reachable and doesn't hold, so +// should be reported as FAILURE + +fn negate(x: i32) -> i32 { + -x +} + +fn main() { + negate(std::i32::MIN); +} diff --git a/tests/expected/reach/overflow-neg/reachable_pass/expected b/tests/expected/reach/overflow-neg/reachable_pass/expected new file mode 100644 index 000000000000..ff43ca409150 --- /dev/null +++ b/tests/expected/reach/overflow-neg/reachable_pass/expected @@ -0,0 +1 @@ +SUCCESS diff --git a/tests/expected/reach/overflow-neg/reachable_pass/test.rs b/tests/expected/reach/overflow-neg/reachable_pass/test.rs new file mode 100644 index 000000000000..e3caea618648 --- /dev/null +++ b/tests/expected/reach/overflow-neg/reachable_pass/test.rs @@ -0,0 +1,16 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular + +// This test checks that kani injects a reachability check for negation +// overflow checks and that it reports ones that are unreachable +// The negation overflow check in this test is reachable, so should be +// reported as SUCCESS + +fn negate(x: i32) -> i32 { + if x != std::i32::MIN { -x } else { std::i32::MAX } +} + +fn main() { + negate(7532); +} diff --git a/tests/expected/reach/overflow-neg/unreachable/expected b/tests/expected/reach/overflow-neg/unreachable/expected new file mode 100644 index 000000000000..7703d171eb67 --- /dev/null +++ b/tests/expected/reach/overflow-neg/unreachable/expected @@ -0,0 +1 @@ +UNREACHABLE diff --git a/tests/expected/reach/overflow-neg/unreachable/test.rs b/tests/expected/reach/overflow-neg/unreachable/test.rs new file mode 100644 index 000000000000..6af515fa8722 --- /dev/null +++ b/tests/expected/reach/overflow-neg/unreachable/test.rs @@ -0,0 +1,16 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular + +// This test checks that kani injects a reachability check for negation +// overflow checks and that it reports ones that are unreachable +// The negation overflow check in this test is unreachable, so should be +// reported as UNREACHABLE + +fn negate(x: i32) -> i32 { + if x != std::i32::MIN { -x } else { std::i32::MAX } +} + +fn main() { + negate(std::i32::MIN); +} diff --git a/tests/expected/reach/overflow/reachable_fail/expected b/tests/expected/reach/overflow/reachable_fail/expected new file mode 100644 index 000000000000..ff09b04f4770 --- /dev/null +++ b/tests/expected/reach/overflow/reachable_fail/expected @@ -0,0 +1,2 @@ +FAILURE +Failed Checks: attempt to subtract with overflow diff --git a/tests/expected/reach/overflow/reachable_fail/test.rs b/tests/expected/reach/overflow/reachable_fail/test.rs new file mode 100644 index 000000000000..1cd350f84f21 --- /dev/null +++ b/tests/expected/reach/overflow/reachable_fail/test.rs @@ -0,0 +1,17 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular + +// This test checks that kani injects a reachability check for arithmetic +// overflow checks and that it reports ones that are unreachable. +// The arithmetic overflow check in this test is reachable but does not hold, so +// should be reported as FAILURE + +fn cond_reduce(thresh: u32, x: u32) -> u32 { + if x > thresh { x - 50 } else { x } +} + +fn main() { + cond_reduce(60, 70); + cond_reduce(40, 42); +} diff --git a/tests/expected/reach/overflow/reachable_pass/expected b/tests/expected/reach/overflow/reachable_pass/expected new file mode 100644 index 000000000000..ff43ca409150 --- /dev/null +++ b/tests/expected/reach/overflow/reachable_pass/expected @@ -0,0 +1 @@ +SUCCESS diff --git a/tests/expected/reach/overflow/reachable_pass/test.rs b/tests/expected/reach/overflow/reachable_pass/test.rs new file mode 100644 index 000000000000..910ee5efd2ee --- /dev/null +++ b/tests/expected/reach/overflow/reachable_pass/test.rs @@ -0,0 +1,19 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular + +// This test checks that kani injects a reachability check for arithmetic +// overflow checks and that it reports ones that are unreachable. +// The arithmetic overflow check in this test is reachable, so should be +// reported as SUCCESS + +fn reduce(x: u32) -> u32 { + if x > 1000 { x - 1000 } else { x } +} + +fn main() { + reduce(7); + reduce(33); + reduce(728); + reduce(1079); +} diff --git a/tests/expected/reach/overflow/unreachable/expected b/tests/expected/reach/overflow/unreachable/expected new file mode 100644 index 000000000000..7703d171eb67 --- /dev/null +++ b/tests/expected/reach/overflow/unreachable/expected @@ -0,0 +1 @@ +UNREACHABLE diff --git a/tests/expected/reach/overflow/unreachable/test.rs b/tests/expected/reach/overflow/unreachable/test.rs new file mode 100644 index 000000000000..b44f81e2a6c1 --- /dev/null +++ b/tests/expected/reach/overflow/unreachable/test.rs @@ -0,0 +1,18 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular + +// This test checks that kani injects a reachability check for arithmetic +// overflow checks and that it reports ones that are unreachable +// The arithmetic overflow check in this test is unreachable, so should be +// reported as UNREACHABLE + +fn reduce(x: u32) -> u32 { + if x > 1000 { x - 1000 } else { x } +} + +fn main() { + reduce(7); + reduce(33); + reduce(728); +} diff --git a/tests/expected/reach/rem-zero/reachable_fail/expected b/tests/expected/reach/rem-zero/reachable_fail/expected new file mode 100644 index 000000000000..c1577e467633 --- /dev/null +++ b/tests/expected/reach/rem-zero/reachable_fail/expected @@ -0,0 +1,2 @@ +FAILURE +Failed Checks: attempt to calculate the remainder with a divisor of zero diff --git a/tests/expected/reach/rem-zero/reachable_fail/test.rs b/tests/expected/reach/rem-zero/reachable_fail/test.rs new file mode 100644 index 000000000000..c7ea17f8dd82 --- /dev/null +++ b/tests/expected/reach/rem-zero/reachable_fail/test.rs @@ -0,0 +1,16 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks + +// This test checks that kani injects a reachability check for +// remainder-by-zero checks and that it reports ones that are unreachable. +// The check in this test is reachable and doesn't hold, so should be reported +// as FAILURE + +fn rem(x: u16, y: u16) -> u16 { + x % y +} + +fn main() { + rem(678, 0); +} diff --git a/tests/expected/reach/rem-zero/reachable_pass/expected b/tests/expected/reach/rem-zero/reachable_pass/expected new file mode 100644 index 000000000000..ff43ca409150 --- /dev/null +++ b/tests/expected/reach/rem-zero/reachable_pass/expected @@ -0,0 +1 @@ +SUCCESS diff --git a/tests/expected/reach/rem-zero/reachable_pass/test.rs b/tests/expected/reach/rem-zero/reachable_pass/test.rs new file mode 100644 index 000000000000..758facbadf47 --- /dev/null +++ b/tests/expected/reach/rem-zero/reachable_pass/test.rs @@ -0,0 +1,15 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks + +// This test checks that kani injects a reachability check for +// remainder-by-zero checks and that it reports ones that are unreachable. +// The check in this test is reachable, so should be reported as SUCCESS + +fn rem(x: u16, y: u16) -> u16 { + if y != 0 { x % y } else { 0 } +} + +fn main() { + rem(11, 3); +} diff --git a/tests/expected/reach/rem-zero/unreachable/expected b/tests/expected/reach/rem-zero/unreachable/expected new file mode 100644 index 000000000000..7703d171eb67 --- /dev/null +++ b/tests/expected/reach/rem-zero/unreachable/expected @@ -0,0 +1 @@ +UNREACHABLE diff --git a/tests/expected/reach/rem-zero/unreachable/test.rs b/tests/expected/reach/rem-zero/unreachable/test.rs new file mode 100644 index 000000000000..0e470eba4070 --- /dev/null +++ b/tests/expected/reach/rem-zero/unreachable/test.rs @@ -0,0 +1,15 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --assertion-reach-checks --output-format regular --no-default-checks + +// This test checks that kani injects a reachability check for +// remainder-by-zero checks and that it reports ones that are unreachable. +// The check in this test is unreachable, so should be reported as UNREACHABLE + +fn rem(x: u16, y: u16) -> u16 { + if y != 0 { x % y } else { 0 } +} + +fn main() { + rem(5, 0); +}