3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Commit graph

143 commits

Author SHA1 Message Date
Dan Liew
7c99721b60 [TravisCI] Don't run Python regression tests under ASan for now.
The script that runs them doesn't propagate LD_PRELOAD and so the
tests fail.
2017-10-16 13:21:03 +01:00
Dan Liew
a1b6316e2e [TravisCI] Try to unbreak running Python regression tests under ASan. 2017-10-16 09:49:54 +01:00
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
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
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
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
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
Dan Liew
0be28b66fe [TravisCI] Update out of date README.md file. 2017-10-06 12:57:46 +01:00
Dan Liew
2519719d3f Fix typo 2017-10-06 12:57:46 +01:00
Dan Liew
d47aea3987 [TravisCI] Workaround slow unit test execution for Debug builds.
Unit tests execute very slowly in Debug (i.e. unoptimized) builds.  This
causes TravisCI to terminate the job due to no console output being
seen.

To workaround this for the debug builds the tests are just compiled
but not executed. To implement this the `RUN_UNIT_TESTS` environment
variable now can take on the values `BUILD_ONLY`, `BUILD_AND_RUN`,
and `SKIP` rather than `0` or `1`.
2017-10-06 12:57:42 +01:00
Dan Liew
0633d5819f [TravisCI] Fix bug. PYTHON_EXECUTABLE should not be in common
defaults. The location is dependent on the implementation.

This triggered a build failure on TravisCI because the location
of the default Python binary is different to what is in the Docker
container.
2017-10-05 15:09:16 +01:00
Dan Liew
eb975a49d6 [TravisCI] Fix bug where Z3_BUILD_TYPE was not being passed as
a Docker build argument.

Also update an out of date comment.
2017-10-05 14:56:31 +01:00
Dan Liew
53fc6ac11b [TravisCI] Refactor as many CI default options as possible so that
the Docker and "TravisCI macOS" builds share most of the same defaults
by sourcing the `ci_defaults.sh` file.
2017-10-05 14:56:15 +01:00
Dan Liew
850c2ebc0c [TravisCI] Add scripts to build and test Z3 on macOS (OSX) and
add a single configuration to TravisCI to test.

TravisCI is very slow at running macOS jobs so just have one
configuration for now.
2017-08-12 19:14:06 +01:00
Dan Liew
cbca609af4 [TravisCI] Fix running unit tests.
Previously the `test-z3` executable was run without arguments which
appears to run no tests. To fix this the `/a` argument is passed
which will run all tests that don't require arguments.

This was noticed in #1159 when @KarenHuang2016 reported a failing
test.
2017-07-26 08:57:46 +01:00
Dan Liew
630863619b [TravisCI] Add Z3_WARNINGS_AS_ERRORS environment variable to
control the `WARNINGS_AS_ERRORS` CMake option.
2017-07-09 14:44:20 +01:00
Dan Liew
8310fed528 [TravisCI] Implement TravisCI build and testing infrastructure for Linux
The Linux builds rely on Docker (using Ubuntu 16.04LTS and Ubuntu
14.04LTS) to build and test Z3 so that builds are easily reproducible.

A build status button has been added to `README.md` so that it is
easy to see the current build status.

More documentation can be found in `contrib/ci/README.md`.

This implementation currently tests 13 different configurations. If
build times become too long we can remove some of them.

Although it would be nice to test macOS builds that requires
significantly more work so I have left this as future work.
2017-07-01 11:51:30 +01:00
Dan Liew
5c3b11f034 [CMake] Modify contrib/cmake/bootstrap.py to do nothing except
print a warning.

Now that the CMake files have been moved into their intended location
it is no longer necessary for this script to exist.

However we do not want to break out-of-tree scripts that build Z3 using
CMake to suddenly break. So the script has been modified to do nothing
except print a warning.

Eventually we should remove this script.
2017-06-12 11:59:39 +01:00
Dan Liew
4b517b96df [CMake] Move CMake files into their intended location so the
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
2017-06-12 11:59:00 +01:00
Nikolaj Bjorner
edb164587f get rid of a simplifier dependency
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-23 10:12:32 -07:00
Nikolaj Bjorner
f1f0f78617 remove foci reference from cmakelist.txt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-19 18:31:34 -07:00
Nikolaj Bjorner
64f3b3e316 remove lp_main from test branch to ensure test build only builds a single entry point
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-12 07:59:16 -07:00
Nikolaj Bjorner
905cf08e5d missing files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 14:11:33 -07:00
Nikolaj Bjorner
911b24784a merge LRA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 10:46:11 -07:00
Nikolaj Bjorner
8eb26e25c2 add new files to cmakelist.txt files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-05 17:03:03 -04:00
Dan Liew
1db07f1189 [CMake] Remove BYPRODUCTS declaration for api_docs target.
This breaks the `clean` rule when using Ninja as the CMake
generator. Unfortunately this means `clean` doesn't try to
remove the generated documentation anymore when using Ninja.
2017-05-04 15:29:47 +01:00
Dan Liew
6e07d6dd2d [CMake] Override CMake's default flags for GCC/Clang as we were doing
before 4cc2b292c0.

It's useful to be able to control the defaults and CMake's internal
logic for GCC/Clang is simple enough that doing this makes sense.

It would be nice to do the same for MSVC but CMake's internal
logic is more complicated so for now it's better that we just use
CMake's default.
2017-04-29 17:45:02 +01:00
Dan Liew
2a919cf16e [CMake] Duplicate the remaining linker flags from the old build system. 2017-04-29 16:22:46 +01:00
Dan Liew
d032dbcbb2 [CMake] When using MSVC set the /SUBSYSTEM: argument given to
the linker. This mimics the behaviour of the old build system.
2017-04-29 16:22:46 +01:00
Dan Liew
364bcde6c1 [CMake] When building with MSVC pass the /STACK: argument to the
linker like the old build system does.
2017-04-29 16:22:46 +01:00
Dan Liew
c9aac0ba77 [CMake] When building with MSVC try to disable incremental linking
for all builds.
2017-04-29 16:22:46 +01:00
Dan Liew
5893aea602 [CMake] When building with MSVC and without WARNINGS_AS_ERRORS
pass `/WX-` to MSVC. Although this is not necessary this duplicates
the behaviour of the old build system.
2017-04-29 16:22:46 +01:00