- I'm using structs directly from the C code.
- - The comments in the upstream code translate into predicates.
+ - The upstream comments translate into machine-checkable code.
The first upstream function is:
and using the predicates we can write a specification:
- $ less snippets/range_is_empty.c
+ $ cat snippets/range_is_empty.c
And we can compile and prove that: