Add DDVerify models and benchmarks

[sim642]

This imports DDVerify from http://www.cprover.org/ddverify/.

TODO

• Remove concurrency stubs (pthread, spinlock, semaphore, mutex).
• Generate main harnesses for all 31 drivers.
• Remove seq1 and con2 models? Or at least extract common model.
• Join thread before calling exit? Probably not, if exit should join everything on its own.
• Spawn more than one thread? Possibly not, since multiple interrupts cannot run in parallel.

Problems

• cciss: wait undeclared.
• cdu31a: init returns with error, harness never starts.
• pcwd: ioctl never called. (Fix unsound dereferencing of unknown pointer offset chain in DDVerify analyzer#684)