Concrete Playback=inplace produces unit test inside the harness #2450
Description
When I invoke concrete playback with Kani 0.28, the unit test is produced inside the harness instead of after it. Happens regardless of where the harness is placed (inside a module, outside of it).
using the following command line invocation:
kani /home/ubuntu/rectangle_example/src/main.rs --harness stretched_rectangle_can_hold_original --enable-unstable --concrete-playback=inplace
with Kani version: 0.28
I expected to see this happen: the unit test should be placed after the harness
#[kani::proof]
pub fn stretched_rectangle_can_hold_original() {
let original = Rectangle {
width: kani::any(),
height: kani::any(),
};
let factor = kani::any();
if let Some(larger) = original.stretch(factor) {
assert!(larger.can_hold(&original));
}
}
#[test]
fn kani_concrete_playback_stretched_rectangle_can_hold_original_7840735556438970593() {
let concrete_vals: Vec<Vec<u8>> = vec![
// 0ul
vec![0, 0, 0, 0, 0, 0, 0, 0],
// 1ul
vec![1, 0, 0, 0, 0, 0, 0, 0],
// 9223372036854841360ul
vec![16, 0, 1, 0, 0, 0, 0, 128],
];
kani::concrete_playback_run(concrete_vals, stretched_rectangle_can_hold_original);
}Instead, this happened: the unit test was placed inside the harness
#[kani::proof]
pub fn stretched_rectangle_can_hold_original() {
#[test]
fn kani_concrete_playback_stretched_rectangle_can_hold_original_7840735556438970593() {
let concrete_vals: Vec<Vec<u8>> = vec![
// 0ul
vec![0, 0, 0, 0, 0, 0, 0, 0],
// 1ul
vec![1, 0, 0, 0, 0, 0, 0, 0],
// 9223372036854841360ul
vec![16, 0, 1, 0, 0, 0, 0, 128],
];
kani::concrete_playback_run(concrete_vals, stretched_rectangle_can_hold_original);
}
let original = Rectangle {
width: kani::any(),
height: kani::any(),
};
let factor = kani::any();
if let Some(larger) = original.stretch(factor) {
assert!(larger.can_hold(&original));
}
}