mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 10:19:23 +00:00
Code Activity
7555 commits 46 branches 52 tags 178 MiB
Commit graph

7555 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
40dfdb6606 bypass UBSan error warnings by using nullptr as error handler. Has same no-op effect. Issue #1287 2017-10-13 07:38:04 -07:00