diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 4fce3f7494b6..8e0e23e0334c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -48,6 +48,9 @@ pub enum PropertyClass { /// /// SPECIAL BEHAVIOR: "Errors" for this type of assertion just mean "reachable" not failure. Cover, + /// Same codegen as `Cover`, but failure will cause verification failure. + /// Used internally for contract instrumentation; see the contracts module in kani_macros for details. + ContractCover, /// The class of checks used for code coverage instrumentation. Only needed /// when working on coverage-related features. /// @@ -150,6 +153,12 @@ impl GotocCtx<'_> { self.codegen_assert(cond.not(), PropertyClass::Cover, msg, loc) } + /// Generate a cover statement for a contract at the current location + pub fn codegen_contract_cover(&self, cond: Expr, msg: &str, span: SpanStable) -> Stmt { + let loc = self.codegen_caller_span_stable(span); + self.codegen_assert(cond.not(), PropertyClass::ContractCover, msg, loc) + } + /// Generate a cover statement for code coverage reports. pub fn codegen_coverage( &self, diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 7d63315e1e13..a88d12e794a0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -82,6 +82,45 @@ impl GotocHook for Cover { } } +/// A hook for Kani's `contract_cover` function. +/// This is only used internally for contract instrumentation. +/// We use it to check that a contract's preconditions are satisfiable and that its postconditions are reachable. +/// Unlike the standard `cover`, failing this check does cause verification failure. +struct ContractCover; +impl GotocHook for ContractCover { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { + matches_function(tcx, instance.def, "KaniContractCover") + } + + fn handle( + &self, + gcx: &mut GotocCtx, + _instance: Instance, + mut fargs: Vec, + _assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + assert_eq!(fargs.len(), 2); + let cond = fargs.remove(0).cast_to(Type::bool()); + let msg = fargs.remove(0); + let msg = gcx.extract_const_message(&msg).unwrap(); + let target = target.unwrap(); + let caller_loc = gcx.codegen_caller_span_stable(span); + + let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span); + + Stmt::block( + vec![ + reach_stmt, + gcx.codegen_contract_cover(cond, &msg, span), + Stmt::goto(bb_label(target), caller_loc), + ], + caller_loc, + ) + } +} + struct Assume; impl GotocHook for Assume { fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { @@ -594,6 +633,7 @@ pub fn fn_hooks() -> GotocHooks { hooks: vec![ Rc::new(Panic), Rc::new(Assume), + Rc::new(ContractCover), Rc::new(Assert), Rc::new(Check), Rc::new(Cover), diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index a34f6815e3dd..17e29a04297f 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -95,6 +95,7 @@ pub struct PropertyId { } impl Property { + const CONTRACT_COVER_PROPERTY_CLASS: &'static str = "contract_cover"; const COVER_PROPERTY_CLASS: &'static str = "cover"; const COVERAGE_PROPERTY_CLASS: &'static str = "code_coverage"; @@ -102,6 +103,11 @@ impl Property { self.property_id.class.clone() } + /// Returns true if this is an contract_cover property + pub fn is_contract_cover_property(&self) -> bool { + self.property_id.class == Self::CONTRACT_COVER_PROPERTY_CLASS + } + // Returns true if this is a code_coverage check pub fn is_code_coverage_property(&self) -> bool { self.property_id.class == Self::COVERAGE_PROPERTY_CLASS diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 5c10d08badb6..7334ef780080 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -512,8 +512,8 @@ pub fn postprocess_result(properties: Vec, extra_ptr_checks: bool) -> let updated_properties = update_properties_with_reach_status(properties_filtered, has_fundamental_failures); - let results_after_code_coverage = update_results_of_code_covererage_checks(updated_properties); - update_results_of_cover_checks(results_after_code_coverage) + let results_after_code_coverage = update_results_of_code_coverage_checks(updated_properties); + update_results_of_cover_checks(results_after_code_coverage, has_failed_unwinding_asserts) } /// Determines if there is property with status `FAILURE` and the given description @@ -623,7 +623,7 @@ fn update_properties_with_reach_status( /// Note that these statuses are intermediate statuses that aren't reported to /// users but rather internally consumed and reported finally as `PARTIAL`, `FULL` /// or `NONE` based on aggregated line coverage results. -fn update_results_of_code_covererage_checks(mut properties: Vec) -> Vec { +fn update_results_of_code_coverage_checks(mut properties: Vec) -> Vec { for prop in properties.iter_mut() { if prop.is_code_coverage_property() { prop.status = match prop.status { @@ -647,7 +647,17 @@ fn update_results_of_code_covererage_checks(mut properties: Vec) -> Ve /// Note that if the cover property was unreachable, its status at this point /// will be `CheckStatus::Unreachable` and not `CheckStatus::Success` since /// `update_properties_with_reach_status` is called beforehand -fn update_results_of_cover_checks(mut properties: Vec) -> Vec { +/// +/// Although regular cover properties do not fail verification, contract cover properties do. +/// If the assert(!cond) is unreachable or successful, then fail. +/// Also fail if the status is undetermined and there are failed unwinding asserts; if we didn't unwind enough, +/// we know that the postcondition is unreachable. +/// If the status is undetermined for another reason (e.g., unsupported constructs), leave the result as undetermined. +/// If the status is failure (as expected), succeed. +fn update_results_of_cover_checks( + mut properties: Vec, + has_failed_unwinding_asserts: bool, +) -> Vec { for prop in properties.iter_mut() { if prop.is_cover_property() { if prop.status == CheckStatus::Success { @@ -655,6 +665,15 @@ fn update_results_of_cover_checks(mut properties: Vec) -> Vec() -> T { - // This function should not be reacheable. + // This function should not be reachable. // Users must include `#[kani::recursion]` in any function contracts for recursive functions; // otherwise, this might not be properly instantiate. We mark this as unreachable to make // sure Kani doesn't report any false positives. @@ -291,7 +291,7 @@ macro_rules! kani_intrinsics { /// function, both cause Kani to produce a warning since we don't support caller location. /// (see https://github.com/model-checking/kani/issues/2010). /// - /// This function is dead, since its caller is always handled via a hook anyway, + /// This function is dead, since its caller is always handled via a hook anyway, /// so we just need to put a body that rustc does not complain about. /// An infinite loop works out nicely. fn kani_intrinsic() -> T { @@ -346,6 +346,14 @@ macro_rules! kani_intrinsics { } } + /// This function is only used for function contract instrumentation. + /// It is the same as cover(), but if the cover statement is unreachable, it fails the contract harness. + /// See the contracts module in kani_macros for details. + #[inline(never)] + #[rustc_diagnostic_item = "KaniContractCover"] + #[doc(hidden)] + pub const fn contract_cover(_cond: bool, _msg: &'static str) {} + /// A way to break the ownerhip rules. Only used by contracts where we can /// guarantee it is done safely. #[inline(never)] @@ -383,7 +391,7 @@ macro_rules! kani_intrinsics { #[inline(never)] #[doc(hidden)] pub unsafe fn write_any(_pointer: *mut T) { - // This function should not be reacheable. + // This function should not be reachable. // Users must include `#[kani::recursion]` in any function contracts for recursive functions; // otherwise, this might not be properly instantiate. We mark this as unreachable to make // sure Kani doesn't report any false positives. diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 863cf882f063..7804825a2550 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -25,6 +25,7 @@ impl<'a> ContractConditionsHandler<'a> { ContractConditionsData::Requires { attr } => { quote!({ kani::assume(#attr); + kani::internal::contract_cover(#attr, "The contract's precondition is satisfiable."); #(#body_stmts)* }) } @@ -46,6 +47,7 @@ impl<'a> ContractConditionsHandler<'a> { #(#assumes)* #remembers #(#rest_of_body)* + kani::internal::contract_cover(#ensures_clause, "The contract's postcondition is reachable."); #exec_postconditions #return_expr }) diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index 41be536ffb6d..d0d9bfc96ed6 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -58,6 +58,10 @@ //! added before the body and postconditions after as well as injected before //! every `return` (see [`PostconditionInjector`]). All arguments are captured //! by the closure. +//! We also inject contract_cover checks after the precondition and before the postcondition. +//! The precondition cover checks ensure that the precondition is satisfiable; i.e., +//! that the precondition does not empty the search space and produce a vacuous proof. +//! The postcondition cover checks ensure that the postcondition is reachable. //! //! ## Replace Function //! @@ -169,6 +173,7 @@ //! || -> u32 //! { //! kani::assume(divisor != 0); +//! kani::internal::contract_cover(divisor != 0, "The contract's precondition is satisfiable."); //! let _wrapper_arg = (); //! #[kanitool::is_contract_generated(wrapper)] //! #[allow(dead_code, unused_variables, unused_mut)] @@ -176,6 +181,11 @@ //! |_wrapper_arg| -> u32 { dividend / divisor }; //! let result_kani_internal: u32 = //! __kani_modifies_div(_wrapper_arg); +//! kani::internal::contract_cover( +//! kani::internal::apply_closure(|result: &u32| +//! *result <= dividend, +//! &result_kani_internal), +//! "The contract's postcondition is reachable."); //! kani::assert(kani::internal::apply_closure(|result: &u32| //! *result <= dividend, &result_kani_internal), //! "|result : &u32| *result <= dividend"); @@ -211,6 +221,7 @@ //! || -> u32 //! { //! kani::assume(divisor != 0); +//! kani::internal::contract_cover(divisor != 0, "The contract's precondition is satisfiable."); //! let _wrapper_arg = (); //! #[kanitool::is_contract_generated(wrapper)] //! #[allow(dead_code, unused_variables, unused_mut)] @@ -218,6 +229,11 @@ //! |_wrapper_arg| -> u32 { dividend / divisor }; //! let result_kani_internal: u32 = //! __kani_modifies_div(_wrapper_arg); +//! kani::internal::contract_cover( +//! kani::internal::apply_closure(|result: &u32| +//! *result <= dividend, +//! &result_kani_internal), +//! "The contract's postcondition is reachable."); //! kani::assert(kani::internal::apply_closure(|result: &u32| //! *result <= dividend, &result_kani_internal), //! "|result : &u32| *result <= dividend"); @@ -311,6 +327,7 @@ //! || //! { //! kani::assume(*ptr < 100); +//! kani::internal::contract_cover(*ptr < 100, "The contract's precondition is satisfiable."); //! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; //! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; //! let _wrapper_arg = (ptr as *const _,); @@ -320,9 +337,21 @@ //! |_wrapper_arg| { *ptr += 1; }; //! let result_kani_internal: () = //! __kani_modifies_modify(_wrapper_arg); +//! kani::internal::contract_cover( +//! kani::internal::apply_closure(|result| +//! (remember_kani_internal_2e780b148d45b5c8) == * ptr, +//! &result_kani_internal +//! ), +//! "The contract's postcondition is reachable."); //! kani::assert(kani::internal::apply_closure(|result| //! (remember_kani_internal_92cc419d8aca576c) == *ptr, //! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); +//! kani::internal::contract_cover( +//! kani::internal::apply_closure(|result| +//! (remember_kani_internal_2e780b148d45b5c8) == * ptr, +//! &result_kani_internal +//! ), +//! "The contract's postcondition is reachable."); //! kani::assert(kani::internal::apply_closure(|result| //! (remember_kani_internal_92cc419d8aca576c) == *ptr, //! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); @@ -367,6 +396,7 @@ //! || //! { //! kani::assume(*ptr < 100); +//! kani::internal::contract_cover(*ptr < 100, "The contract's precondition is satisfiable."); //! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; //! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; //! let _wrapper_arg = (ptr as *const _,); @@ -376,9 +406,21 @@ //! |_wrapper_arg| { *ptr += 1; }; //! let result_kani_internal: () = //! __kani_modifies_modify(_wrapper_arg); +//! kani::internal::contract_cover( +//! kani::internal::apply_closure(|result| +//! (remember_kani_internal_2e780b148d45b5c8) == * ptr, +//! &result_kani_internal +//! ), +//! "The contract's postcondition is reachable."); //! kani::assert(kani::internal::apply_closure(|result| //! (remember_kani_internal_92cc419d8aca576c) == *ptr, //! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); +//! kani::internal::contract_cover( +//! kani::internal::apply_closure(|result| +//! (remember_kani_internal_2e780b148d45b5c8) == * ptr, +//! &result_kani_internal +//! ), +//! "The contract's postcondition is reachable."); //! kani::assert(kani::internal::apply_closure(|result| //! (remember_kani_internal_92cc419d8aca576c) == *ptr, //! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); diff --git a/tests/expected/function-contract/cover_contract/never_type_fixme.expected b/tests/expected/function-contract/cover_contract/never_type_fixme.expected new file mode 100644 index 000000000000..53e2ce503bf7 --- /dev/null +++ b/tests/expected/function-contract/cover_contract/never_type_fixme.expected @@ -0,0 +1,9 @@ +contract_cover.2\ + - Status: FAILURE\ + - Description: "The contract's postcondition is reachable." + +unwind.0\ + - Status: FAILURE\ + - Description: "unwinding assertion loop 0" + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/cover_contract/never_type_fixme.rs b/tests/expected/function-contract/cover_contract/never_type_fixme.rs new file mode 100644 index 000000000000..d14f3173ab3a --- /dev/null +++ b/tests/expected/function-contract/cover_contract/never_type_fixme.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Unreachable postcondition because the function never returns. +// Kani should fail verification because the postcondition is unreachable, +// but currently doesn't generate the postcondition check at all +// (although verification still fails because of the unwinding error). +// We may need special never type detection for this case. + +#![feature(never_type)] + +#[kani::requires(true)] +#[kani::ensures(|result: &!| true)] +fn never_return() -> ! { + let x = 7; + loop {} +} + +// Unreachable postcondition because the function never returns +#[kani::proof_for_contract(never_return)] +#[kani::unwind(5)] +fn prove_never_return() { + never_return(); +} diff --git a/tests/expected/function-contract/cover_contract/undetermined_postcondition.expected b/tests/expected/function-contract/cover_contract/undetermined_postcondition.expected new file mode 100644 index 000000000000..6d7541ff1b23 --- /dev/null +++ b/tests/expected/function-contract/cover_contract/undetermined_postcondition.expected @@ -0,0 +1,9 @@ + +contract_cover.2\ + - Status: UNDETERMINED\ + - Description: "The contract's postcondition is reachable." + +unsupported_construct.1\ + - Status: FAILURE + +VERIFICATION:- FAILED \ No newline at end of file diff --git a/tests/expected/function-contract/cover_contract/undetermined_postcondition.rs b/tests/expected/function-contract/cover_contract/undetermined_postcondition.rs new file mode 100644 index 000000000000..e3d27a36ac56 --- /dev/null +++ b/tests/expected/function-contract/cover_contract/undetermined_postcondition.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Test `cover_contract` functionality, which fails verification for a unsatisfiable precondition +// or unreachable postcondition. +// See https://github.com/model-checking/kani/issues/2793 + +// Undetermined whether we can reach the postcondition because we encounter an unsupported construct. + +#[kani::proof_for_contract(unsupp)] +fn undetermined_example() { + let mut x = 0; + unsupp(&mut x); + assert!(x == 0); +} + +#[kani::requires(true)] +#[kani::ensures(|res| *res == *x)] +fn unsupp(x: &mut u8) -> u8 { + unsafe { + std::arch::asm!("nop"); + } + *x +} diff --git a/tests/expected/function-contract/cover_contract/unreachable_postcondition.expected b/tests/expected/function-contract/cover_contract/unreachable_postcondition.expected new file mode 100644 index 000000000000..fd4ed7de24d3 --- /dev/null +++ b/tests/expected/function-contract/cover_contract/unreachable_postcondition.expected @@ -0,0 +1,24 @@ + +contract_cover.1\ + - Status: FAILURE\ + - Description: "The contract's postcondition is reachable." + +unwind.0\ + - Status: FAILURE\ + - Description: "unwinding assertion loop 0" + +VERIFICATION:- FAILED + +assertion.1\ + - Status: FAILURE\ + - Description: "panic" + +contract_cover.1\ + - Status: SUCCESS\ + - Description: "The contract's precondition is satisfiable." + +contract_cover.2\ + - Status: FAILURE\ + - Description: "The contract's postcondition is reachable." + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/cover_contract/unreachable_postcondition.rs b/tests/expected/function-contract/cover_contract/unreachable_postcondition.rs new file mode 100644 index 000000000000..182a5e90b207 --- /dev/null +++ b/tests/expected/function-contract/cover_contract/unreachable_postcondition.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Test `cover_contract` functionality, which fails verification for a unsatisfiable precondition +// or unreachable postcondition. +// See https://github.com/model-checking/kani/issues/2793 + +// Test that verification fails for an unreachable postcondition. + +// The precondition is satisfiable, but the postcondition is unreachable because the code panics. +// Test that in the case where the postcondition check's property status is unreachable (because the function panics) +// we change the status to failure. +#[kani::requires(a > 5)] +#[kani::ensures(|result: &u32| *result == a)] +fn unreachable_postcondition(a: u32) -> u32 { + panic!("panic") +} + +#[kani::proof_for_contract(unreachable_postcondition)] +fn prove_unreachable_postcondition() { + let x: u32 = kani::any(); + unreachable_postcondition(x); +} + +// Unreachable postcondition because the function never returns. +// Test that in the case where the postcondition check's property status is undetermined because of unwinding failures, +// we change the status to failure. +#[kani::ensures(|result: &u32| *result == 7)] +fn never_return() -> u32 { + loop {} + 7 +} + +#[kani::proof_for_contract(never_return)] +#[kani::unwind(5)] +fn prove_never_return() { + never_return(); +} diff --git a/tests/expected/function-contract/cover_contract/unsatisfiable_precondition.expected b/tests/expected/function-contract/cover_contract/unsatisfiable_precondition.expected new file mode 100644 index 000000000000..fa9a2a1d2e8a --- /dev/null +++ b/tests/expected/function-contract/cover_contract/unsatisfiable_precondition.expected @@ -0,0 +1,23 @@ +contract_cover.1\ + - Status: FAILURE\ + - Description: "The contract's precondition is satisfiable." + +contract_cover.2\ + - Status: FAILURE\ + - Description: "The contract's postcondition is reachable." + +VERIFICATION:- FAILED + +contract_cover.1\ + - Status: SUCCESS\ + - Description: "The contract's precondition is satisfiable." + +contract_cover.2\ + - Status: FAILURE\ + - Description: "The contract's precondition is satisfiable." + +contract_cover.3\ + - Status: FAILURE\ + - Description: "The contract's postcondition is reachable." + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/cover_contract/unsatisfiable_precondition.rs b/tests/expected/function-contract/cover_contract/unsatisfiable_precondition.rs new file mode 100644 index 000000000000..80b7ac3b0e5c --- /dev/null +++ b/tests/expected/function-contract/cover_contract/unsatisfiable_precondition.rs @@ -0,0 +1,38 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Test `cover_contract` functionality, which fails verification for an unsatisfiable precondition +// or unreachable postcondition. +// See https://github.com/model-checking/kani/issues/2793 + +// Test that verification fails for unsatisfiable preconditions. + +// Unsatisfiable precondition; separate requires clauses. +// The postcondition is unreachable because of the unsatisfiable precondition. +#[kani::requires(a > 5)] +#[kani::requires(a < 4)] +#[kani::ensures(|result: &u32| *result == a)] +fn separate_requires(a: u32) -> u32 { + panic!("This code is never tested") +} + +#[kani::proof_for_contract(separate_requires)] +fn prove_separate_requires() { + let x: u32 = kani::any(); + separate_requires(x); +} + +// Unsatisfiable precondition; single requires clause +// The postcondition is unreachable because of the unsatisfiable precondition. +#[kani::requires(a > 5 && a < 4)] +#[kani::ensures(|result: &u32| *result == a)] +fn conjoined_requires(a: u32) -> u32 { + panic!("This code is never tested") +} + +#[kani::proof_for_contract(conjoined_requires)] +fn prove_conjoined_requires() { + let x: u32 = kani::any(); + conjoined_requires(x); +} diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected index 4014a0723029..094dc6b7993e 100644 --- a/tests/expected/function-contract/valid_ptr.expected +++ b/tests/expected/function-contract/valid_ptr.expected @@ -1,5 +1,8 @@ Checking harness pre_condition::harness_invalid_ptr... -VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) +contract_cover.1\ + - Status: FAILURE\ + - Description: "The contract's precondition is satisfiable." +VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected) Checking harness pre_condition::harness_stack_ptr... VERIFICATION:- SUCCESSFUL @@ -7,4 +10,8 @@ VERIFICATION:- SUCCESSFUL Checking harness pre_condition::harness_head_ptr... VERIFICATION:- SUCCESSFUL -Complete - 3 successfully verified harnesses, 0 failures, 3 total +Checking harness post_condition::harness... +assertion.1\ + - Status: FAILURE\ + - Description: "|result| kani::mem::can_dereference((*result).0)" +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/valid_ptr.rs b/tests/expected/function-contract/valid_ptr.rs index 2047a46caf4f..af49b5cd053b 100644 --- a/tests/expected/function-contract/valid_ptr.rs +++ b/tests/expected/function-contract/valid_ptr.rs @@ -35,12 +35,9 @@ mod pre_condition { } } -/// TODO: Enable once we fix: -#[cfg(not_supported)] mod post_condition { - /// This contract should fail since we are creating a dangling pointer. - #[kani::ensures(kani::mem::can_dereference(result.0))] + #[kani::ensures(|result| kani::mem::can_dereference((*result).0))] unsafe fn new_invalid_ptr() -> PtrWrapper { let var = 'c'; PtrWrapper(&var as *const _)