Add DDVerify models and benchmarks - Githubissues

goblint / bench

The benchmark suite

4 stars 5 forks source link

Add DDVerify models and benchmarks #26

Open sim642 opened 2 years ago

sim642 commented 2 years ago

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

TODO

[x] Remove concurrency stubs (pthread, spinlock, semaphore, mutex).
[x] 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. (https://github.com/goblint/analyzer/pull/684)