The benchmarks in this directory were generated with DDVerify, which is described in the paper

Thomas Witkowski, Nicolas Blanc, Daniel Kroening, and Georg Weissenbacher.
Model Checking Concurrent Linux Device Drivers.
Proc. ASE, pages 501-504, 2007. ACM.

There is one separate file for each assertion in file ddv_machzwd_all.i
(i.e., _all contains all claims).
The other postfixes indicate the name of the function in which the
assertion occurs.

*.i   The files have been (slightly) pre-processed with CIL.

*.cil.c - CIL-preprocessed sources (32-bit machine architecture)

cilly --printCilAsIs --domakeCFG --dosimplify --no-convert-field-offsets --save-temps --no-convert-direct-calls --envmachine

CIL_MACHINE=short=2,2 int=4,4 long=4,4 long_long=8,4 pointer=4,4 enum=4,4 float=4,4 double=8,4 long_double=12,4 void=1 bool=1,1 fun=1,1 alignof_string=1 max_alignment=16 size_t=unsigned_int wchar_t=int char_signed=true const_string_literals=true big_endian=false __thread_is_keyword=true __builtin_va_list=true underscore_name=false