On 06/14/2017 07:02 PM, Dan Williams wrote: > On Wed, Jun 14, 2017 at 9:53 AM, Vlastimil Babka <[email protected]> wrote: > > Can you share the test-thp.c so I can add this to my test collection?
Attached. > I'm assuming cbmc is "Bounded Model Checker for C/C++"? Yes. This blog from Paul inspired me: http://paulmck.livejournal.com/38997.html Works nicely, just if it finds a bug, the counterexamples are a bit of PITA to decipher :) Vlastimil _______________________________________________ Linux-nvdimm mailing list [email protected] https://lists.01.org/mailman/listinfo/linux-nvdimm
