model: rework assert_bug() and assert_user_bug() interfaces
authorBrian Norris <banorris@uci.edu>
Fri, 16 Nov 2012 22:58:32 +0000 (14:58 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 16 Nov 2012 22:58:32 +0000 (14:58 -0800)
commitdc0339b4449ed07afa7c69936108146d72676a68
tree3f9b6fbb6acc9050458708234d68d4c0aa25f26e
parentecf16617a0c289981925fcd2437595f3a2fce8fe
model: rework assert_bug() and assert_user_bug() interfaces

We don't need assert_bug_immediate(), and we don't need some of the
optional parameters in assert_bug(). Just simplify down to two
interfaces:

    assert_bug()
    assert_user_bug()

The former is useful for all bugs triggered from model-checker threads,
and the latter is useful from a user-thread context, so that you can
immediately switch to the model-checking context and exit the program -
but *only if* the trace is currently-feasible.
common.cc
model.cc
model.h