From 75fefa9761336e961fdc59b7f8c1b42f5dbae5b9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 13:59:55 +0000 Subject: [PATCH] fixme test no longer is a fixme-test --- ...2.rs => cast_abstract_args_to_concrete.rs} | 0 .../cast_abstract_args_to_concrete_fixme.rs | 24 ------------------- 2 files changed, 24 deletions(-) rename tests/kani/Cast/{cast_abstract_args_to_concrete_fixme2.rs => cast_abstract_args_to_concrete.rs} (100%) delete mode 100644 tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs diff --git a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs b/tests/kani/Cast/cast_abstract_args_to_concrete.rs similarity index 100% rename from tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs rename to tests/kani/Cast/cast_abstract_args_to_concrete.rs diff --git a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs b/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs deleted file mode 100644 index faeb74c5d66a..000000000000 --- a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs +++ /dev/null @@ -1,24 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! This test is a modified version of cast_abstract_args_to_concrete_fixme.rs. -//! The original test requires --no-undefined-function-checks to pass. This is an issue that -//! require investigation. See https://github.com/model-checking/kani/issues/555. -//! -//! Once this issue is fixed. Please remove this test and remove the kani flag from the original -//! test: --no-undefined-function-check - -fn main() { - let _x32 = 1.0f32.powi(2); - let _x64 = 1.0f64.powi(2); - - unsafe { - let size: libc::size_t = mem::size_of::(); - let my_num: *mut libc::c_void = libc::malloc(size); - if my_num.is_null() { - panic!("failed to allocate memory"); - } - let my_num2 = libc::memset(my_num, 1, size); - libc::free(my_num); - } -}