Dan Liew
88fb31ac08
[TravisCI] Add RUN_API_EXAMPLES
option so that we can disable
...
building/running examples in some configurations.
2017-10-16 08:56:17 +01:00
Dan Liew
dbb7f616c1
More LSan workarounds.
2017-10-16 08:56:17 +01:00
Dan Liew
e51ce8bcaf
[TravisCI] Try again to not show suppressions by default
2017-10-16 08:56:17 +01:00
Dan Liew
ead6e56d15
[TravisCI] Swap run_quiet
and run_non_native_binding
. In the
...
previous order `grep` inside `run_quiet` would get ASan LD_PRELOAD'ed
which would sometimes fail.
2017-10-16 08:56:17 +01:00
Dan Liew
ecadef6e48
[TravisCI] Try to fix case in run_quiet
where the script would fail
...
with.
```
-ne: unary operator expected
```
2017-10-16 08:56:17 +01:00
Dan Liew
ad2a0a0085
[TravisCI] Don't print sanitizer suppressions by default because
...
that breaks Z3's regression tests.
2017-10-16 08:56:17 +01:00
Dan Liew
35f6746c60
Workaround regressions/smt2/error.smt2
test timing out.
...
When ASan's LeakSanitizer is enabled leak checking is triggered
when `exit()` is called and it returns so many false positives that
it takes a long time to write them to the console.
To workaround this we simply call `_Exit()` instead.
2017-10-16 08:56:17 +01:00
Dan Liew
fd98593a58
[ASan] Ignore Clang OpenMP leaks for now.
2017-10-16 08:56:17 +01:00
Dan Liew
2dd1a4046d
[TravisCI] Fix typo
2017-10-16 08:56:17 +01:00
Dan Liew
fd391e75a6
[TravisCI] Fix Z3_BUILD_TYPE
variable that was not propagated
...
into the Docker image as an environment variable.
2017-10-16 08:56:17 +01:00
Dan Liew
675a3ae9dd
[UBSan] Remove a bunch of suppressions.
2017-10-16 08:56:17 +01:00
Dan Liew
db7b2e989d
[TravisCI] Try to run the Python and .NET examples under ASan.
2017-10-16 08:56:17 +01:00
Dan Liew
8d600050db
[LSan] Remove suppression files. The were fixed on rebase
2017-10-16 08:56:17 +01:00
Dan Liew
ff5df20deb
[LSan] Don't run c_maxsat_example
with LeakSanitizer because
...
it contains leaks that the Z3 developers don't intend to fix.
2017-10-16 08:56:17 +01:00
Dan Liew
f90fe928af
[LSan] Suppress another leak until I can figure out what is going on.
2017-10-16 08:56:17 +01:00
Dan Liew
bcff86a316
[LSan] Add suppression for part of #1297 .
2017-10-16 08:56:17 +01:00
Dan Liew
a991e44a25
[TravisCI] Fix typo in created directory for suppression files
2017-10-16 08:56:17 +01:00
Dan Liew
5bcdea1ae5
[TravisCI] For ASan/LSan use larger context so we get larger stack
...
traces if needed.
2017-10-16 08:56:17 +01:00
Dan Liew
38d9e2df84
[TravisCI] Make ASan/UBSan configuration a debug build.
2017-10-16 08:56:17 +01:00
Dan Liew
11f7298c52
[TravisCI] Add ASan configuration
2017-10-16 08:56:17 +01:00
Dan Liew
157c8064e8
[CMake] When building C/C++ API examples use the same build type
...
as Z3 if doing a single configuration build.
2017-10-16 08:56:17 +01:00
Dan Liew
4db5980a23
[TravisCI] Fix getting proper stack traces for ASan/LSan. The
...
`llvm-symbolizer` tool needs to be installed and ASan/LSan needs
to be told where to find it.
2017-10-16 08:56:17 +01:00
Dan Liew
71dcec3113
[UBSan] Update UBSan suppression file to suppress all undefined
...
behaviour I have observed running in CI.
2017-10-16 08:56:17 +01:00
Dan Liew
9455391f1f
[TravisCI] Don't run the python binding system tests when building
...
with UBSan.
This is a workaround. We can't fix this unless we build libz3 with
a shared UBSan runtime.
2017-10-16 08:56:17 +01:00
Dan Liew
f756bf6c86
[TravisCI] Fix undefined SCRIPT_DIR variable
2017-10-16 08:56:17 +01:00
Dan Liew
fb3d4cfed9
[TravisCI] Add a UBSan configuration
2017-10-16 08:56:17 +01:00
Dan Liew
f15766baee
[TravisCI] Don't run the non-native example when building with UBSan.
...
This a workaround. Right now `libz3` gets linked against a static
UBSan runtime which means none of the non-native language bindings
(e.g. python) can load `libz3` due to undefined symbols. We need
to link `libz3` against a shared UBSan runtime to fix this.
2017-10-16 08:56:17 +01:00
Dan Liew
a9fcfc531b
[TravisCI][CMake] Add Z3_C_EXAMPLES_FORCE_CXX_LINKER
CMake option
...
and propagate its value into the C API examples.
This flag forces the C API examples to use the C++ compiler as the
linker rather than the C compiler. This a workaround to avoid linking
errors when building with UBSan.
2017-10-16 08:56:17 +01:00
Dan Liew
64ee9f168d
[TravisCI] Add ASan/LSan/UBSan suppression files and use them in
...
CI.
2017-10-16 08:56:17 +01:00
Nikolaj Bjorner
b63754e362
adding explicit assignment for auto-generated function.
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-15 21:16:54 -07:00
Nikolaj Bjorner
0aa12b9423
Merge pull request #1300 from nunoplopes/master
...
fix vector<> to support non-POD types
2017-10-15 20:51:49 -07:00
Nuno Lopes
2905bdebef
make vector friendly to gcc < 5
2017-10-16 00:54:31 +01:00
Nuno Lopes
6cefb700ac
add move constructor to ref_vector
2017-10-16 00:54:31 +01:00
Nuno Lopes
82b25a0608
add move constructor to watch_list
2017-10-16 00:54:31 +01:00
Nuno Lopes
d18e975a49
vector: make expand_vector() less prone to mem leaks by calling the destructors after move
2017-10-16 00:54:30 +01:00
Nuno Lopes
e7f0f3b834
add move constructor to obj_ref
2017-10-16 00:54:30 +01:00
Nuno Lopes
29acec672f
nnf: remove ast incref
2017-10-16 00:54:30 +01:00
Nuno Lopes
6c2d0394ac
add move constructor to rational
2017-10-16 00:54:30 +01:00
Nuno Lopes
912a729097
fix build of unit tests
2017-10-16 00:54:30 +01:00
Nuno Lopes
468e0207f7
add move constructor to mpf
2017-10-16 00:54:30 +01:00
Nuno Lopes
d1c13f17b0
remove noexcept since MSVC 2012 doest support it
2017-10-16 00:54:30 +01:00
Nuno Lopes
b53d69be18
fpa_rewriter: remove a mpq copy
2017-10-16 00:54:30 +01:00
Nuno Lopes
3cc6dd1cbd
bv_decl_plugin: remove mem allocation
2017-10-16 00:54:29 +01:00
Nuno Lopes
d30a099cd0
fix crash in vector::expand()
2017-10-16 00:54:29 +01:00
Nuno Lopes
27e84c5ffc
mpz.h: fix typo in previous commit (found by Nikolaj)
2017-10-16 00:54:29 +01:00
Nuno Lopes
9b54b4e784
fix vector<> to support non-POD types
...
adjust code to std::move and avoid unnecessary/illegal
2017-10-16 00:54:29 +01:00
Nikolaj Bjorner
4d1acadabb
fix leaks reported in #1309
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-15 09:56:21 -07:00
Nikolaj Bjorner
44be1501ff
Merge branch 'master' of https://github.com/z3prover/z3
2017-10-14 11:59:18 -07:00
Nikolaj Bjorner
7f8a7c3d83
fix the fixme of #1307
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-14 11:59:09 -07:00
Nikolaj Bjorner
5b6472f022
change nullptr to 0
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-13 10:54:29 -07:00