Michael Hicks

type of calloc in stdlib_checked.h

4

In `stdlib_checked.h` the function `calloc` is defined thus: ``` extern _Itype_for_any(T) void *calloc(size_t nmemb, size_t size) : itype(_Array_ptr) byte_count(nmemb * size); ``` but this type fails to recognize that since...

Field access to structs with bounded and NT char arrays

5

I have code like this: ``` struct mystr { _Array_ptr buf : count(len); unsigned int len; }; int getlen(_Ptr p_str) { return p_str->len; } _Nt_array_ptr getbuf(_Ptr p_str) { return p_str->buf;...

How to use `Arbitrary` generators?

7

I saw that PR #108 that includes `Arbitrary` generator support, but I didn't see corresponding instructions for how to leverage it. In particular, I'd like to use values generated by...

I'm trying to use VSCoq along with QuickChick. I am getting an error that when trying to run QuickChick it cannot find `ocamlbuild` in order to build and execute the...