Sanjit Bhat

The current deterministic values parser in `kani-driver/src/exe_trace.rs` works on arbitrary `serde::Value` types. This means that if we expect certain `Value` blobs to be arrays, we have to test for that...

See title. This would improve the user experience if we consider generated test cases to be short-lived. We could either remove all generated test cases or only test cases without...

This feature is experimental rather than unstable. Unstable implies that it has soundness issues or something like that.

We currently require there to be only one harness when adding det tests to the source code. This feature fixes that.

See title. Exe trace was the old name, but det playback is more representative of the feature right now.

Add compiletest mode that runs E2E concrete playback tests

1

See title. This involves adding a new `compiletest` mode for these kinds of tests.

See title. This needs to: 1. Separate `modify_src_code` into smaller functions. 2. Add unit tests for `modify_src_code` and `format_unit_test`.

Change `kani::any::<bool>()` to make the non-det bit pattern more intuitive

9

## TLDR This issue proposes changing our implementation of `kani::any::()` from: https://github.com/model-checking/kani/blob/de71c097f266053d6b10c1c4d762b47766a210d9/library/kani/src/arbitrary.rs#L48-L54 to something like ```rust impl Arbitrary for bool { #[inline(always)] fn any() -> Self { let byte =...

C AST generalizer doesn't allow void functions

1

**TLDR**: If you run the Transpyler AST Generalizer on a C program with `void` functions, it will throw an `isinstance` assertion error because `pycparser` returns `None` for the function declaration,...