projects / model-checker.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b35625b) | patch
test/uninit: add an "uninit" test
authorBrian Norris <banorris@uci.edu>
Wed, 12 Dec 2012 02:38:16 +0000 (18:38 -0800)
committerBrian Norris <banorris@uci.edu>
Wed, 12 Dec 2012 02:38:16 +0000 (18:38 -0800)
commitf41ab746f55e04e33a15c41fa61aa084d2f98ed2
treec0e4b1b01359c7aefa9b8828f977328edf344179tree | snapshot
parentb35625b0499717b3caab5344d7278a31fbee9cb6commit | diff
test/uninit: add an "uninit" test

This is a weird example, where we don't explicitly initialize y, but
synchronization should guarantee that it is initialized.

Right now, this example has a problem where we never see flag == 2.
test/uninit.cc [new file with mode: 0644] blob
C++11 memory model checker