3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Commit graph

644 commits

Author SHA1 Message Date
Nikolaj Bjorner
888699548d
Revert "Specify encoding of source files in mk_util.py" 2018-05-03 11:59:49 -07:00
Carsten Varming
c279fd9f2e Specify encoding of source files in mk_util.py 2018-05-02 23:27:33 -04:00
Nikolaj Bjorner
c513f3ca09 merge with master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-25 14:57:01 -07:00
Pierre Pronchery
5f7bd993de Add support for NetBSD
Originally from David Holland <dholland@NetBSD.org>.
2018-03-13 21:59:35 +01:00
Nikolaj Bjorner
0ce2001449 fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-10 11:39:22 -08:00
Christoph M. Wintersteiger
0ef33a98c4
Revert "Fix encoding error" 2018-02-13 14:08:55 +00:00
Virgile ROBLES
fddc4e311f
Fix encoding error
The encode/decode is not needed and fails if any non-ASCII character is returned by g++ or clang++
2018-01-26 00:30:59 +01:00
Ivan Gotovchits
49678065bd fixes compilation flags for OCaml plugins
The `-linkall` option is needed for a plugin to be standalone,
otherwise it will miss those dependencies that are not used.
2017-12-13 14:45:06 -05:00
Christoph M. Wintersteiger
7c63a5cc1d Fixed MSYS/MinGW build. Fixes #1335. 2017-11-11 16:38:53 +00:00
Christoph M. Wintersteiger
45975bec65 Improved support for MSYS/MINGW. Fixes #969. 2017-11-11 15:11:54 +00:00
Christoph M. Wintersteiger
19f43713c9 Fixed Windows build of C example. 2017-11-08 21:16:03 +00:00
Christoph M. Wintersteiger
bec6c3f9e2 Fixed C example build. 2017-11-08 18:22:17 +00:00
Christoph M. Wintersteiger
a8b52419f5 Fixed C example build. 2017-11-08 18:14:42 +00:00
Nikolaj Bjorner
fd49a0c89c added facility to persist model transformations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-02 00:05:52 -05:00
Paul Ehrlich
2a459c5ff6 MSYS offers a MINGW shell as well. (uses different os.uname()) 2017-11-01 12:02:48 +01:00
Christoph M. Wintersteiger
e50470f2c4 Added support for MSYS2 2017-10-30 18:24:38 +00:00
Nikolaj Bjorner
c1b243a8e3 merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-07 19:24:30 +01:00
Nikolaj Bjorner
a625301a41 expose incremental cubing over API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-09-28 15:05:10 -07:00
Christoph M. Wintersteiger
9a464dded4 Removed -std=c++11 from OCaml stubs build command. Fixes #1263. 2017-09-27 14:22:59 +01:00
Nikolaj Bjorner
e1d08e9526 remove reinterpret cast occurrences that require disabling strict alias analysis #987 #1210
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-17 20:41:29 -07:00
Nuno Lopes
4b00bc636b revert the patch to remove no-strict-aliasing
VS 2012 doesnt support C++11 unions..
2017-08-14 23:00:59 +01:00
Nuno Lopes
2473c69679 Drop no-strict-aliasing and fix 2 places where it was violated 2017-08-14 20:09:49 +01:00
Christoph M. Wintersteiger
6bc5209e26 Fixed build problems with .vcxproj 2017-08-01 15:53:55 +01:00
Daniel Perelman
d57494395c Add --guardcf flag to mk_make.py to optionally enable Control Flow Guard. 2017-07-06 16:59:20 -07:00
Dan Liew
d00892c9a6 [CMake] Fix dependencies for generating mem_initializer.cpp.
Previously CMake was not aware of which headers files the generation
of `mem_initializer.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declare memory initializers/finalizers change.
* New headers are added that declare memory initializers/finalizer.

Now the `z3_add_component()` CMake function has been modifed so that
it now takes an optional `MEMORY_INIT_FINALIZER_HEADERS` argument
which allows the headers that declare memory initializers/finalizers
to be explicitly listed.

With this information CMake will now regenerate `mem_initializer.cpp`
correctly.

This required the `mk_mem_initializer_cpp_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
2017-06-21 23:56:53 +01:00
Dan Liew
6f48a145aa [CMake] Fix dependencies for generating gparams_register_modules.cpp.
Previously CMake was not aware of which headers files the generation
of `gparams_register_modules.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declared module description/parameters change.
* New headers are added that declare module description/parameters.
* `.pyg` files that generate header files that declare module
  description/parameters change

Now the `z3_add_component()` CMake function has been modifed so that

* All header files that are generated from `.pyg` files are added as
dependencies and are scanned from module description/parameter
declarations. This implicit dependency of `gparams_register_modules.cpp`
depending on other generated header files seems unnecessary complex. We
should revisit this design decision once the Python/Makefile build
system is deprecated.

* The function now takes an optional `EXTRA_REGISTER_MODULE_HEADERS`
argument which allows the headers that declare module
description/paramters to be explicitly listed.

With this information CMake will now regenerate `gparams_register_modules.cpp`
correctly.

This required the `mk_gparams_register_modules_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
2017-06-21 23:56:46 +01:00
Dan Liew
229fd3dc3e [CMake] Fix dependencies for generating install_tactic.cpp.
Previously CMake was not aware of which headers files the generation
of `install_tactic.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declared tactics/probes changed.
* New tactics/probes were added to new header files.

Now the `z3_add_component()` CMake function has been modifed to take an
optional `TACTIC_HEADERS` argument which allows the headers that declare
tactics/probes to be explicitly listed. The necessary component
declarations have been modified to declare their tactic/probe header
files.

With this information CMake will now regenerate `install_tactic.cpp`
correctly.

This required the `mk_install_tactic_cpp_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
2017-06-21 23:03:48 +01:00
Nikolaj Bjorner
691788f449 remove stale references to foci
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-19 20:21:08 -07:00
Christoph M. Wintersteiger
a258236229 Disabled debug output 2017-05-19 18:51:52 +01:00
Christoph M. Wintersteiger
46791047fa Fixed VS 2017 platform toolset version in .vcxproj 2017-05-12 14:28:55 +01:00
Nikolaj Bjorner
a64a73255e make source directory relative to build directory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 15:46:24 -07:00
Nikolaj Bjorner
7731163d11 use forward slash on src include
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 14:42:43 -07:00
Nikolaj Bjorner
911b24784a merge LRA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 10:46:11 -07:00
Christoph M. Wintersteiger
79dcf03a42 Enabled C++11 in GCC and Clang 2017-05-05 15:01:10 +01:00
Christoph M. Wintersteiger
0ebce66c57 Fixed bug with .NET keyfile path containing spaces. Fixes #1003. 2017-05-05 14:22:40 +01:00
Christoph M. Wintersteiger
3bbe5eceeb fix for --get-describe 2017-03-24 15:53:46 +00:00
Michael Lowell Roberts
3415672f31 fixed bug where mk_make.py --build=... would fail to handle absolute paths correctly. 2017-02-28 08:24:35 -08:00
Christoph M. Wintersteiger
59db0bc9c4 Merge pull request #829 from legendtang/fix_utf8_conf
Fixed utf-8 version string handling for python2. Resolved #787
2017-02-04 20:38:51 +00:00
Christoph M. Wintersteiger
b9bfd4ddf5 Merge pull request #854 from angr/fix/fpic-arm
Add -fpic to armv7/armv8 build
2017-01-18 21:55:52 +00:00
Andrew Dutcher
1eec0799ca Add -fpic to armv7/armv8 build 2016-12-22 14:26:41 -08:00
Dan Liew
2e74a2c54e Refactor update_api.mk_ml() so that the source and output directories
can be different. This feature will be needed by the CMake build system
to build the OCaml bindings.
2016-12-19 21:05:17 +00:00
Dan Liew
76bbecf4fe Refactor mk_z3consts_ml() code into mk_z3consts_ml_internal()
and move that into `mk_genfile_common.py`. Then adapt `mk_util.py` and
`mk_consts_files.py` to call into the code at its new location.

The purpose of this change is to have Python code common to the Python
and CMake build systems separate from Python code that is only used for
the Python build system.
2016-12-19 21:05:17 +00:00
Dan Liew
0e03fe9bf2 Fix inconsistent emission of OCaml enumeration files. The ordering of emitted
enum values is not consistent between python 2 or 3. The root cause
of the problem was a dictionary's keys being iterated over which has
no defined order.

This has been fixed by iterating over the dictionary's items and
ordering by values.  We could order by key rather than the values but
seeing as these represent an enum, ordering by value makes more sense.
2016-12-19 21:05:16 +00:00
Christoph M. Wintersteiger
251d1ec031 Fix for parallel builds of the OCaml API. Relates to #797. 2016-12-19 16:58:25 +00:00
Christoph M. Wintersteiger
2c32e30fed Build fix for static binaries + shared examples 2016-12-19 16:47:28 +00:00
Christoph M. Wintersteiger
a1a662b23f Build fix for C/C++ example programs. 2016-12-16 04:51:07 -08:00
Christoph M. Wintersteiger
649d474686 Build fix for C++ example 2016-12-09 19:09:47 +00:00
Wensheng Tang
99d10d1224 Fixed utf-8 version string handling for python2. Resolved #787 2016-12-08 15:09:59 +08:00
Nuno Lopes
1d417f6527 fix warnings in configure script 2016-11-23 09:32:20 +00:00
Christoph M. Wintersteiger
dee7c29b19 Added optional synchronization for multi-thread API logs. Relates to #798. 2016-11-22 11:32:25 +00:00