Skip to content

Commit 8cb3b04

Browse files
author
Carolyn Zech
committed
fix filter test
the compiler can derive arbitrary now, so update the test accordingly
1 parent 5d6c016 commit 8cb3b04

2 files changed

Lines changed: 40 additions & 26 deletions

File tree

‎tests/script-based-pre/cargo_autoharness_filter/filter.expected‎

Lines changed: 26 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
Kani generated automatic harnesses for 42 function(s):
1+
Kani generated automatic harnesses for 43 function(s):
22
+--------------------------+----------------------------------------------+
33
| Crate | Selected Function |
44
+=========================================================================+
@@ -10,6 +10,8 @@ Kani generated automatic harnesses for 42 function(s):
1010
|--------------------------+----------------------------------------------|
1111
| cargo_autoharness_filter | yes_harness::f_char |
1212
|--------------------------+----------------------------------------------|
13+
| cargo_autoharness_filter | yes_harness::f_compiler_derives_arbitrary |
14+
|--------------------------+----------------------------------------------|
1315
| cargo_autoharness_filter | yes_harness::f_derives_arbitrary |
1416
|--------------------------+----------------------------------------------|
1517
| cargo_autoharness_filter | yes_harness::f_f128 |
@@ -89,25 +91,25 @@ Kani generated automatic harnesses for 42 function(s):
8991

9092
Kani did not generate automatic harnesses for 8 function(s).
9193
If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832
92-
+--------------------------+----------------------------------------+------------------------------------------------------------------------------+
93-
| Crate | Skipped Function | Reason for Skipping |
94-
+==================================================================================================================================================+
95-
| cargo_autoharness_filter | no_harness::doesnt_implement_arbitrary | Missing Arbitrary implementation for argument(s) x: DoesntImplementArbitrary |
96-
|--------------------------+----------------------------------------+------------------------------------------------------------------------------|
97-
| cargo_autoharness_filter | no_harness::unsupported_const_pointer | Missing Arbitrary implementation for argument(s) _y: *const i32 |
98-
|--------------------------+----------------------------------------+------------------------------------------------------------------------------|
99-
| cargo_autoharness_filter | no_harness::unsupported_generic | Generic Function |
100-
|--------------------------+----------------------------------------+------------------------------------------------------------------------------|
101-
| cargo_autoharness_filter | no_harness::unsupported_mut_pointer | Missing Arbitrary implementation for argument(s) _y: *mut i32 |
102-
|--------------------------+----------------------------------------+------------------------------------------------------------------------------|
103-
| cargo_autoharness_filter | no_harness::unsupported_no_arg_name | Missing Arbitrary implementation for argument(s) _: &() |
104-
|--------------------------+----------------------------------------+------------------------------------------------------------------------------|
105-
| cargo_autoharness_filter | no_harness::unsupported_ref | Missing Arbitrary implementation for argument(s) _y: &i32 |
106-
|--------------------------+----------------------------------------+------------------------------------------------------------------------------|
107-
| cargo_autoharness_filter | no_harness::unsupported_slice | Missing Arbitrary implementation for argument(s) _y: &[u8] |
108-
|--------------------------+----------------------------------------+------------------------------------------------------------------------------|
109-
| cargo_autoharness_filter | no_harness::unsupported_vec | Missing Arbitrary implementation for argument(s) _y: std::vec::Vec<u8> |
110-
+--------------------------+----------------------------------------+------------------------------------------------------------------------------+
94+
+--------------------------+----------------------------------------+----------------------------------------------------------------------------------+
95+
| Crate | Skipped Function | Reason for Skipping |
96+
+======================================================================================================================================================+
97+
| cargo_autoharness_filter | no_harness::doesnt_implement_arbitrary | Missing Arbitrary implementation for argument(s) x: DoesntImplementArbitrary<'_> |
98+
|--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
99+
| cargo_autoharness_filter | no_harness::unsupported_const_pointer | Missing Arbitrary implementation for argument(s) _y: *const i32 |
100+
|--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
101+
| cargo_autoharness_filter | no_harness::unsupported_generic | Generic Function |
102+
|--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
103+
| cargo_autoharness_filter | no_harness::unsupported_mut_pointer | Missing Arbitrary implementation for argument(s) _y: *mut i32 |
104+
|--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
105+
| cargo_autoharness_filter | no_harness::unsupported_no_arg_name | Missing Arbitrary implementation for argument(s) _: &() |
106+
|--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
107+
| cargo_autoharness_filter | no_harness::unsupported_ref | Missing Arbitrary implementation for argument(s) _y: &i32 |
108+
|--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
109+
| cargo_autoharness_filter | no_harness::unsupported_slice | Missing Arbitrary implementation for argument(s) _y: &[u8] |
110+
|--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
111+
| cargo_autoharness_filter | no_harness::unsupported_vec | Missing Arbitrary implementation for argument(s) _y: std::vec::Vec<u8> |
112+
+--------------------------+----------------------------------------+----------------------------------------------------------------------------------+
111113

112114
Autoharness: Checking function yes_harness::f_tuple against all possible inputs...
113115
Autoharness: Checking function yes_harness::f_maybe_uninit against all possible inputs...
@@ -130,6 +132,7 @@ Autoharness: Checking function yes_harness::f_f128 against all possible inputs..
130132
Autoharness: Checking function yes_harness::f_f16 against all possible inputs...
131133
Autoharness: Checking function yes_harness::f_f64 against all possible inputs...
132134
Autoharness: Checking function yes_harness::f_f32 against all possible inputs...
135+
Autoharness: Checking function yes_harness::f_compiler_derives_arbitrary against all possible inputs...
133136
Autoharness: Checking function yes_harness::f_char against all possible inputs...
134137
Autoharness: Checking function yes_harness::f_bool against all possible inputs...
135138
Autoharness: Checking function yes_harness::f_isize against all possible inputs...
@@ -167,6 +170,8 @@ Autoharness Summary:
167170
|--------------------------+----------------------------------------------+---------------------------+---------------------|
168171
| cargo_autoharness_filter | yes_harness::f_char | #[kani::proof] | Success |
169172
|--------------------------+----------------------------------------------+---------------------------+---------------------|
173+
| cargo_autoharness_filter | yes_harness::f_compiler_derives_arbitrary | #[kani::proof] | Success |
174+
|--------------------------+----------------------------------------------+---------------------------+---------------------|
170175
| cargo_autoharness_filter | yes_harness::f_derives_arbitrary | #[kani::proof] | Success |
171176
|--------------------------+----------------------------------------------+---------------------------+---------------------|
172177
| cargo_autoharness_filter | yes_harness::f_f128 | #[kani::proof] | Success |
@@ -243,4 +248,4 @@ Autoharness Summary:
243248
|--------------------------+----------------------------------------------+---------------------------+---------------------|
244249
| cargo_autoharness_filter | yes_harness::f_usize | #[kani::proof] | Success |
245250
+--------------------------+----------------------------------------------+---------------------------+---------------------+
246-
Complete - 42 successfully verified functions, 0 failures, 42 total.
251+
Complete - 43 successfully verified functions, 0 failures, 43 total.

‎tests/script-based-pre/cargo_autoharness_filter/src/lib.rs‎

Lines changed: 14 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,13 +4,15 @@
44
// Test that the automatic harness generation feature filters functions correctly,
55
// i.e., that it generates harnesses for a function iff:
66
// - It is not itself a harness
7-
// - All of its arguments implement Arbitrary, either trivially or through a user-provided implementation
7+
// - All of its arguments implement Arbitrary, either trivially,
8+
// through a user-provided implementation, or compiler-derived implementation.
89
// The bodies of these functions are purposefully left as simple as possible;
910
// the point is not to test the generated harnesses themselves,
1011
// but only that we generate the harnesses in the first place.
1112

1213
#![feature(f16)]
1314
#![feature(f128)]
15+
#![allow(dead_code)]
1416

1517
extern crate kani;
1618
use kani::Arbitrary;
@@ -31,14 +33,16 @@ impl Arbitrary for ManuallyImplementsArbitrary {
3133
Self { x: kani::any(), y: kani::any() }
3234
}
3335
}
34-
35-
struct DoesntImplementArbitrary {
36+
struct CompilerDerivesArbitrary {
3637
x: u8,
3738
y: u32,
3839
}
39-
40+
struct DoesntImplementArbitrary<'a> {
41+
x: &'a u8,
42+
y: u32,
43+
}
4044
mod yes_harness {
41-
use crate::{DerivesArbitrary, ManuallyImplementsArbitrary};
45+
use crate::{CompilerDerivesArbitrary, DerivesArbitrary, ManuallyImplementsArbitrary};
4246
use std::marker::{PhantomData, PhantomPinned};
4347
use std::mem::MaybeUninit;
4448
use std::num::NonZero;
@@ -164,6 +168,11 @@ mod yes_harness {
164168
fn f_derives_arbitrary(x: DerivesArbitrary) -> DerivesArbitrary {
165169
x
166170
}
171+
172+
fn f_compiler_derives_arbitrary(x: CompilerDerivesArbitrary) -> CompilerDerivesArbitrary {
173+
x
174+
}
175+
167176
fn f_manually_implements_arbitrary(
168177
x: ManuallyImplementsArbitrary,
169178
) -> ManuallyImplementsArbitrary {

0 commit comments

Comments
 (0)