Here's a fairly ad hoc list, off the top of my head, that one might improve and then use for comparison of tools. The aim is to be discriminating while not being too long. Some answers might need comments, not just yes/no - in many cases a tool might partially implement something (e.g. compound type initialisers) but not fully implement the ISO notion. However, it would be good to keep this short enough that most of the data can be presented in a single table for comparison between tools.
This needs a lightweight format so that that table can be auto-generated from sources that can be separately (and easily) edited for each tool. The questions are defined in template.ml and the answers should be in files like answers_VST.ml. Take care not to edit the question text in the latter. For each answer, there are two strings: one that should be short and appears in the generated table, and another that appears as a template. To regenerate the markdown table, just make (with OCaml installed).
The answers_VST.ml is my transcription of Andrew's slide - it probably needs editing.
This README.md is generated by the above - don't edit it directly.
| VST | Isabelle C-parser | |
|---|---|---|
| integer arithmetic | ||
| usual arithmetic conversions | Y | Y |
| arithmetic UBs | Y | Y |
| ABI variants | some | ? |
| floats | ||
| floating types | Y | n |
| characters and strings | ||
| string literals (incl. potential aliasing) | Y | n |
| C11 character-set features | some | n |
| structured data | ||
| basic structs | Y | Y |
| basic enums | Y | Y |
| basic unions | Y | n |
| struct-as-value memory accesses and arguments/returns | n | Y |
| union-as-value memory accesses and arguments/returns | n | n |
| compound type initialisers | Y | some |
| bitfields | n | n |
| flexible array members | some | n |
| variable length arrays | some | Y |
| control flow | ||
| C loose ISO specification of evaluation order | Y | n |
| loops (for, while, do, break, continue) | Y | Y |
| switch (structured) | Y | Y |
| switch (general) | n | n |
| C goto within a block | n | n |
| C goto leaving a block | n | n |
| C goto entering a block | n | n |
| function pointers | Y | very limited |
| non-local jumps (setjump.h) | n | n |
| signal handling (signal.h) | some | n |
| function calls | ||
| mutable function parameters | Y | Y |
| variadic arguments | some | n |
| function parameters of array type with "static" or * | Y | Y |
| lifetime | ||
| block lifetimes (precise or lifted to function scope) | lifted | n/a |
| thread-local storage | n | n |
| memory object model | ||
| basic model (fully concrete/fully abstract/CompCert block+offset/PNVI-ae-udi/whatever) | CompCert block+offset (PS:?) | Tuch UMM model |
| passing addresses of locals in function calls | Y | n |
| storing addresses of locals (e.g. in globals) | Y | n |
| pointer/integer casts (incl. arith on unused/unused bits) | n | Y |
| pointer arithmetic using offset-of | some? | Y, I think |
| subobject provenance | some? | n |
| effective types | Y | ? |
| uninitialised reads | n | n |
| restrict | some | n |
| register | some | n |
| concurrency | ||
| unsequenced races | some | n |
| idealised SC concurrency | n | |
| C/C++11 | n | |
| Linux-kernel | yes(?) | n |
| volatile | n | |
| other | ||
| C11 generic selection | ||
| multiple compilation units | ||
| standard library | ||
| common (GCC/Clang) non-ISO extensions |