Daniel Schwartz-Narbonne

memcpy compiles to memcpy_chk, which is not recognized by smack

2

When I compile the following code, the function memcpy_chk gets inserted, which is not handled properly by SMACK. ``` #include int test(char* a, char* b, int len) { memcpy(a,b,len); }...

Support `__CPROVER_r_ok`

1

http://cprover.diffblue.com/memory-primitives.html

https://github.com/model-checking/kani/pull/1230

Add a zero_initializer function

6

### Description of changes: Right now, we can only `zero_init` scalar types. This adds a recursive form to allow us to `zero_init` complex types as well. ### Resolved issues: Resolves...

AFAIK, we can only have this case for Enums. Generators use a different field naming scheme, so we would need to specalize this operation for Enum/Generator, if there is a...

https://github.com/todogroup/repolinter/blob/main/docs/rules.md#file-contents

[DRAFT] Support MMIO regions

2

### Description of changes: Adds support for MMIO regions to kani proof harnesses. ### Resolved issues: Resolves #1304 ### Call-outs: - [ ] This is dependent on https://github.com/diffblue/cbmc/pull/6747. It will...