Jacob Salzberg

Is there any chance that variable length arrays (c99) might be supported some time in the future? thanks.

Make this into a cookiecutter(?)

2

I might do this myself if I have to do it, but there is a python program called cookiecutter which is really nice for starting new projects. I think it...

Consider using transient maps over hydras for controlling debugger state

2

Hello! One minor complaint I have about dap-mode is that the hydra that controls the debugger state (e.g. lets you do next, in, disconnect etc) is open even when you...

Can I use this for dos 16 bit?

11

I have a 16 bit dos exe (mz format) that I'd like to extract line number information from. It seems to maybe be dwarf, as it has all of those...

Add DrCCTLib Instruction Analysis Tool

4

I have completed a tool that, in a similar format to drcctlib_instr_statistics, analyzes each instruction in each calling context and categorizes the instructions into groups of memory loads, memory stores,...

Overwriting a composite object in an array causes a blowup in variables

3

The following code: ```rust const MAX_NUM_OBJECTS: usize = 1024; const MAX_OBJECT_SIZE: usize = 64; const STACK_DEPTH: usize = 6; type PtrId = u32; #[derive(Copy, Clone)] enum Item { Even, Odd,...

Stacked Borrows in Kani

2

This PR adds stacked borrows to Kani, strengthening its model of pointers to detect violations of Rust's aliasing model. It does this by automatically instrumenting code with hooks at every...

Enums that are #[repr(u8)] are slower than u8

2

The following code: ```rust #[allow(non_upper_case_globals)] struct DrSeuss; impl DrSeuss { const Thing1: u8 = 0; const Thing2: u8 = 1; } #[kani::proof] fn main() { let mut haystack = [DrSeuss::Thing1;...

Stacked Borrows In Kani -- Extend Feature to handle more code

2

Currently, Stacked Borrows is implemented in the feature branch features/stacked_borrows. However, to merge it into the main code-base, the following updates are needed: 1. We need to add regression tests...