|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Public Member Functions | |
| expand_unittest_main (self, module_node) | |
Protected Member Functions | |
| _collect_test_cases (cls, module_node, modules, case_names) | |
| _expand_main_calls (self, body, names, cases, index) | |
| _build_case_runs (self, cases, source, index) | |
| _inline_assertions (self, module_node, modules, case_names) | |
| _rebound_names (self, module_node) | |
| _is_plain_test_case (self, stmt, modules, known) | |
| _inline_method_assertions (self, method, overridden) | |
| _inline_in_body (self, body, receiver, overridden) | |
| _assertion_claims (self, stmt, receiver, overridden) | |
| _stage_arguments (self, call) | |
Static Protected Member Functions | |
| _unittest_bindings (module_node) | |
| _is_test_case_base (base, modules, case_names) | |
| _is_test_method (node) | |
| _is_main_call (stmt, names) | |
| _assertion_call (stmt, receiver, overridden) | |
| _call (func) | |
Run the test methods `unittest.main()` would discover. The unittest operational model has no runner, so main() is a no-op: a file whose only entry point is `unittest.main()` reaches verification with zero VCCs and reports a vacuous VERIFICATION SUCCESSFUL (#6745). Each discovered test method gets its own instance, as CPython does, so state a test writes in setUp cannot leak into the next one.
|
staticprotected |
The `receiver.assertX(...)` call *stmt* consists of, or None.
|
protected |
The statements that replace an assertX call statement, or None.
|
protected |
|
staticprotected |
|
protected |
(class, sorted test methods) per TestCase subclass, in CPython's order. A subclass runs the tests it inherits as well as its own, so a base class's method is collected again for each subclass -- its setUp may differ. A name redefined in the subclass body is not inherited twice.
|
protected |
Replace each main() in *body* in place; returns the next case index.
|
protected |
Lower `self.assertX(...)` in a TestCase subclass to plain asserts. The model's assertX parameters are Any, which erases a container's type (`first == second` compares two lists by address), so each claim is typed at the call site instead. A call that may reach another assertX -- a name some class here binds or some attribute store sets, or a class with a base, decorator or metaclass outside this module -- stays.
|
protected |
|
protected |
|
staticprotected |
|
protected |
|
staticprotected |
|
staticprotected |
|
protected |
Names a class here binds, and attributes some store sets.
|
protected |
Evaluate each argument once, in source order, as the call would. A constant, and a last argument made of names (isinstance's classes), stay inline: nothing evaluated after them can change their value.
|
staticprotected |
Names bound to the unittest module, to its main() and its TestCase.
| preprocessor.unittest_mixin.UnittestMixin.expand_unittest_main | ( | self, | |
| module_node ) |
Replace every unittest.main() with its discovered test-method calls.