Sacha Ayoun

Add timeout for tests?

3

Adding optional timeouts for tests would be nice (to detect infinite loops for example)

Explore ways of packaging the dependencies correctly

1

Right now, we're vendoring every dependency. However, some dependencies may be annoying, like `uri`, because they themselves have widely-used dependencies (in this case `re`), and we don't want to force...

PATH not properly set in build (Apple Silicon)

1

Hello 😄 **esy version:** 0.6.12 **Operating System:** macOS Monterey 12.4 **Issue:** When installing the project from scratch, user runes into a missing pkg-config or missing python error. Although, looking at...

### Description of changes: Instead of inserting a `comment` field on the Irep for `deinit` and potential future annotations, inserts a `#kani_comment`. It seems that having a field that doesn't...

Add option to enable layout randomization

21

### Description of changes: Randomize layouts by default, but adds a flag to disable that feature. ### Resolved issues: Resolves #1622 (if accepted) ### Call-outs: None that I know of...

Clean GotoC AST annotations

4

Following #1469, it looks like a viable solution for supporting alternative backends is to comment the produced Irep to allow for a different interpretation than CBMC. At the moment, the...

add an uninitialized memory access fixme test

13

### Description of changes: Added `tests/kani/UninitializedMemory/fixme_main.rs` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Kani encodes string slices as null-terminated C slices

2

In Kani's regression test suite, in [offset_u8_ok.rs](https://github.com/model-checking/kani/blob/main/tests/kani/Intrinsics/Offset/offset_u8_ok.rs#L21), an out-of-bound pointer is dereferenced, but not detected by Kani. Here's a reduced code ```rust #![feature(core_intrinsics)] use std::intrinsics::offset; #[kani::proof] fn test_offset() { let...

The `.vscode` fold can contain useful things such as repo-specific configurations that would maybe alleviate the work for new contributors. In particular, I'd like to add a set of recommended...

I just learned that the `-Zrandomize-layout` feature is already out. Even though kani is bit-precise, the analysis shouldn't be depending on specific layouts. Some bugs might be caught by running...