Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add tests for constant-evaluated intrinsics #1042

Merged
merged 10 commits into from
Apr 14, 2022
Merged

Add tests for constant-evaluated intrinsics #1042

Changes from 1 commit
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
bd90c8a
Move test for `needs_drop`
adpaco-aws Apr 13, 2022
38f857c
Minor change to description in `needs_drop` test
adpaco-aws Apr 13, 2022
c4e33a7
Add test for `type_name`
adpaco-aws Apr 13, 2022
66bb55f
Add test for `type_id`
adpaco-aws Apr 13, 2022
ffdbf62
Add test for `size_of`
adpaco-aws Apr 13, 2022
23ba941
Add test for `pref_align_of`
adpaco-aws Apr 13, 2022
31e4c03
Add test for `min_align_of`
adpaco-aws Apr 13, 2022
307dbb0
Include a comment for `codegen_intrinsic_const`
adpaco-aws Apr 13, 2022
ac43650
In `type_id` test, assert no duplicates
adpaco-aws Apr 14, 2022
ee26a0c
Merge branch 'main' into const-eval-audit
adpaco-aws Apr 14, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
58 changes: 35 additions & 23 deletions tests/kani/Intrinsics/ConstEval/type_id.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Check that the `type_id` intrinsic is supported with common data types
// and that there are no duplicate type IDs
#![feature(core_intrinsics)]
use std::intrinsics::type_id;

Expand All @@ -11,27 +12,38 @@ enum MyEnum {}

#[kani::proof]
fn main() {
// Scalar types
let _ = type_id::<i8>();
let _ = type_id::<i16>();
let _ = type_id::<i32>();
let _ = type_id::<i64>();
let _ = type_id::<i128>();
let _ = type_id::<isize>();
let _ = type_id::<u8>();
let _ = type_id::<u16>();
let _ = type_id::<u32>();
let _ = type_id::<u64>();
let _ = type_id::<u128>();
let _ = type_id::<usize>();
let _ = type_id::<f32>();
let _ = type_id::<f64>();
let _ = type_id::<bool>();
let _ = type_id::<char>();
// Compound types (tuple and array)
let _ = type_id::<(i32, i32)>();
let _ = type_id::<[i32; 5]>();
// Custom data types (struct and enum)
let _ = type_id::<MyStruct>();
let _ = type_id::<MyEnum>();
let type_ids = [
// Scalar types
type_id::<i8>(),
type_id::<i16>(),
type_id::<i32>(),
type_id::<i64>(),
type_id::<i128>(),
type_id::<isize>(),
type_id::<u8>(),
type_id::<u16>(),
type_id::<u32>(),
type_id::<u64>(),
type_id::<u128>(),
type_id::<usize>(),
type_id::<f32>(),
type_id::<f64>(),
type_id::<bool>(),
type_id::<char>(),
// Compound types (tuple and array)
type_id::<(i32, i32)>(),
type_id::<[i32; 5]>(),
// Custom data types (struct and enum)
type_id::<MyStruct>(),
type_id::<MyEnum>(),
];

// Check that there are no duplicate type IDs
let i: usize = kani::any();
let j: usize = kani::any();
kani::assume(i < type_ids.len());
kani::assume(j < type_ids.len());
if i != j {
assert_ne!(type_ids[i], type_ids[j]);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice!

}
}