| Age | Commit message (Collapse) | Author |
|---|
|
The initial motivation for this commit was that dump with an invalid tag
was leading to a segfault. The reason for the segfault was as follows:
1. `api::Solver` creates an `ExprManager`, which is stored in a
`unique_ptr` as a class member
2. The `api::Solver` tries to create an SmtEngine instance
3. The `SmtEnginePrivate` constructor subscribes to events in the
NodeManager and starts registering option listeners
4. When the `SmtEnginePrivate` gets to registerSetDumpModeListener, it
registers and notifies the DumpModeListener which calls
Dump::setDumpFromString, which fails with an `OptionException` due to
the invalid tag
5. While propagating the exception through `api::Solver`, the
`ExprManager` is deleted but the non-existent `SmtEnginePrivate` is
still subscribed to its events and there are still option listeners
registered. This leads to a segfault because the NodeManager tries to
notify the `SmtEnginePrivate` about deleted nodes
This commit fixes the issue by catching the `OptionException` in
`SmtEnginePrivate`, unsubscribing the `SmtEnginePrivate` from the
NodeManager events and deleting its option listener registrations before
rethrowing the exception. In addition, it changes the
`Options::registerAndNotify()` method to immediately delete a
registration if notifying the registration resulted in an
``OptionException`` (otherwise only the `ListenerCollection` knows about
the registration and complains about it in its destructor). Finally,
the commit adds a simple regression test for invalid dump tags.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
With older versions of CMake, skipped tests are reported as failures,
which is undesirable. This commit changes the CMakeLists file to only
use the `SKIP_RETURN_CODE` property if a newer version of CMake is used.
|
|
|
|
|
|
|
|
Currently, the run_regression.py script just returns 0 when we skip a
test due to a feature not supported by the current configuration.
Returning 0 marks those tests as passed. To make it more clear which
tests were skipped, this commit adds the `SKIP_RETURN_CODE` [0] property
to the regression tests and changes the regression script to return 77
for skipped tests. The feature is supported since at least CMake 3.0 [0].
For backwards compatibility with autotools, returning 77 for skipped
tests is only active when `--cmake` is passed to the run_regression.py
script.
[0] https://cmake.org/cmake/help/v3.0/prop_test/SKIP_RETURN_CODE.html
|
|
When parsing with `--strict-parsing`, we are checking whether the
operators that we encounter have been explicitly added to the
`d_logicOperators` set in the `Parser` class. We did not do that for the
indexed operator `(_ to_fp ...)` (which is represented by the kind
`FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Targets 'check', 'units', 'systemtests' and 'regress' are now run in
parallel with the number of available cores by default. This can be
overriden by passing ARGS=-jN.
|
|
|
|
|
|
|
|
|
|
|
