8000 Failures when build Z3 with msvc + permissive- on windows · Issue #1616 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Failures when build Z3 with msvc + permissive- on windows #1616

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
PhoebeHui opened this issue May 11, 2018 · 7 comments
Closed

Failures when build Z3 with msvc + permissive- on windows #1616

PhoebeHui opened this issue May 11, 2018 · 7 comments

Comments

@PhoebeHui
Copy link

Z3 failed when build with permissive- by msvc on windows, could you help have a look?

Environment: VS2017 latest version + windows server 2016 + Z3 master branch latest revision

Repro:

  1. git clone https://github.com/Z3Prover/z3 D:\Z3\src
  2. Open a VS 2017 x86 command prompt and browse to d:\Z3
  3. set CL=/permissive-
  4. mkdir build_x86 && pushd build_x86
  5. cmake -G "Visual Studio 15 2017" -DCMAKE_SYSTEM_VERSION=10.0.16299.0 ..\src
  6. msbuild build_x86\Z3.sln /p:Configuration=Release;Platform=Win32 /t:Rebuild /m /p:BuildInParallel=true

Failures like:
D:\Z3\src\src\util/string_buffer.h(85): error C3861: 'ARRAYSIZE': identifier not found
D:\Z3\src\src\util/string_buffer.h(136): note: see reference to class template instantiation 'string_buffer<INITIAL_SIZE>' being compiled
D:\Z3\src\src\util/string_buffer.h(95): error C3861: 'ARRAYSIZE': identifier not found
D:\Z3\src\src\util/string_buffer.h(105): error C3861: 'ARRAYSIZE': identifier not found
@NikolajBjorner
Copy link
Contributor
  1. what breaks if not using /permissive?
  2. do you plan to add a pull request to fix these?

@PhoebeHui
Copy link
Author

For #1, should be /permissive-, no breaks.
For #2, The macro ARRAYSIZE (probably a macro) is not defined when string_buffer.h is included. we're not sure which header this comes from. So no pull request planed here.

@PhoebeHui
Copy link
Author

This issue still affect us, is there any reasons to close this issue?

@NikolajBjorner
Copy link
Contributor

apart from not using " -DCMAKE_SYSTEM_VERSION=10.0.16299.0 ", my build with the current master goes through with these settings.

NikolajBjorner added a commit that referenced this issue Aug 16, 2018
@NikolajBjorner
remove dependency on ARRAYSIZE for issue #1616
2b2f193 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
Copy link
Contributor

I have now also removed references to ARRAYSIZE in the code.

@PhoebeHui
Copy link
Author

Thank you NikolajBjorner for fix this issue!

I will verify the changes, I will let you know the results.

@PhoebeHui
Copy link
Author

I have verified, this issue fixed, thank you NikolajBjorner!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@NikolajBjorner @PhoebeHui
0