mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 17:14:07 +00:00
.net: remove net35 related build props; drop src/api/dotnet/core
This commit is contained in:
Yatao Li
parent
b72cb96ee3
commit
ffd26e5a56
2
.gitignore
vendored
2
.gitignore
vendored
|
|
@ -76,3 +76,5 @@ src/api/ml/z3.mllib
|
|||
*.bak
|
||||
doc/api
|
||||
doc/code
|
||||
.vs
|
||||
examples/**/obj
|
||||
|
|
|
|||
17
CMakeSettings.json
Normal file
17
CMakeSettings.json
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
{
|
||||
"configurations": [
|
||||
{
|
||||
"name": "x64-Release",
|
||||
"generator": "Visual Studio 15 2017 Win64",
|
||||
"configurationType": "RelWithDebInfo",
|
||||
"inheritEnvironments": [
|
||||
"msvc_x64_x64"
|
||||
],
|
||||
"buildRoot": "F:\\b\\z3\\build\\${name}",
|
||||
"installRoot": "F:\\b\\z3\\install\\${name}",
|
||||
"cmakeCommandArgs": "",
|
||||
"buildCommandArgs": "",
|
||||
"ctestCommandArgs": ""
|
||||
}
|
||||
]
|
||||
}
|
||||
|
|
@ -1,7 +1,8 @@
|
|||
<Project>
|
||||
<PropertyGroup>
|
||||
<OutputPath>${_DN_OUTPUT_PATH}/</OutputPath>
|
||||
<XPLAT_LIB_DIR>${XPLAT_LIB_DIR}/</XPLAT_LIB_DIR>
|
||||
<XPLAT_LIB_DIR>${_DN_XPLAT_LIB_DIR}/</XPLAT_LIB_DIR>
|
||||
<DOTNET_PACKAGE_VERSION>${_DN_VERSION}</DOTNET_PACKAGE_VERSION>
|
||||
${_DN_CUSTOM_BUILDPROPS}
|
||||
</PropertyGroup>
|
||||
</Project>
|
||||
|
|
|
|||
|
|
@ -32,9 +32,15 @@
|
|||
# produced by running the .NET program, and can be consumed from other build steps.
|
||||
#
|
||||
# ```
|
||||
# RUN_DOTNET(<project_file>
|
||||
# RUN_DOTNET(<project_file> [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP]
|
||||
# [ARGUMENTS program_args...]
|
||||
# [OUTPUT outputs...])
|
||||
# [OUTPUT outputs...]
|
||||
# [CONFIG configuration]
|
||||
# [PLATFORM platform]
|
||||
# [DEPENDS depend_nuget_packages... ]
|
||||
# [OUTPUT_PATH output_path relative to cmake binary output dir]
|
||||
# [CUSTOM_BUILDPROPS <CustomProp>value</CustomProp>....]
|
||||
# [SOURCES additional_file_dependencies... ])
|
||||
# ```
|
||||
#
|
||||
# ADD_MSBUILD -- add a project to be built by msbuild. Windows-only. When building in Unix systems, msbuild targets are skipped.
|
||||
|
|
@ -54,11 +60,11 @@
|
|||
# Multiple smoke tests will be run one-by-one to avoid global resource conflicts.
|
||||
#
|
||||
# SMOKETEST_DOTNET(<project_file> [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP]
|
||||
# [ARGUMENTS program_args...]
|
||||
# [CONFIG configuration]
|
||||
# [PLATFORM platform]
|
||||
# [PACKAGE output_nuget_packages... ]
|
||||
# [VERSION nuget_package_version]
|
||||
# [DEPENDS depend_nuget_packages... ]
|
||||
# [OUTPUT_PATH output_path relative to cmake binary output dir]
|
||||
# [CUSTOM_BUILDPROPS <CustomProp>value</CustomProp>....]
|
||||
# [SOURCES additional_file_dependencies... ])
|
||||
#
|
||||
|
|
@ -81,7 +87,8 @@
|
|||
#
|
||||
# ```
|
||||
# TEST_DOTNET(<project_file>
|
||||
# [ARGUMENTS additional_dotnet_test_args...])
|
||||
# [ARGUMENTS additional_dotnet_test_args...]
|
||||
# [OUTPUT_PATH output_path relative to cmake binary output dir])
|
||||
# ```
|
||||
#
|
||||
# GEN_DOTNET_PROPS -- Generates a Directory.Build.props file. The created file is populated with MSBuild properties:
|
||||
|
|
@ -153,7 +160,6 @@ FUNCTION(DOTNET_REGISTER_LOCAL_REPOSITORY repo_name repo_path)
|
|||
ENDFUNCTION()
|
||||
|
||||
FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments)
|
||||
FILE(GLOB_RECURSE DOTNET_deps *.cs *.fs *.xaml *.csproj *.fsproj *.tsl)
|
||||
CMAKE_PARSE_ARGUMENTS(
|
||||
# prefix
|
||||
_DN
|
||||
|
|
@ -166,18 +172,29 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments)
|
|||
# the input arguments
|
||||
${arguments})
|
||||
|
||||
GET_FILENAME_COMPONENT(_DN_abs_proj "${_DN_PROJECT}" ABSOLUTE)
|
||||
GET_FILENAME_COMPONENT(_DN_proj_dir "${_DN_abs_proj}" DIRECTORY)
|
||||
GET_FILENAME_COMPONENT(_DN_projname "${_DN_PROJECT}" NAME)
|
||||
STRING(REGEX REPLACE "\\.[^.]*$" "" _DN_projname_noext ${_DN_projname})
|
||||
|
||||
FILE(GLOB_RECURSE DOTNET_deps
|
||||
${_DN_proj_dir}/*.cs
|
||||
${_DN_proj_dir}/*.fs
|
||||
${_DN_proj_dir}/*.vb
|
||||
${_DN_proj_dir}/*.xaml
|
||||
${_DN_proj_dir}/*.resx
|
||||
${_DN_proj_dir}/*.xml
|
||||
${_DN_proj_dir}/*.*proj
|
||||
${_DN_proj_dir}/*.cs
|
||||
${_DN_proj_dir}/*.config)
|
||||
LIST(APPEND DOTNET_deps ${_DN_SOURCES})
|
||||
SET(_DN_deps "")
|
||||
FOREACH(dep ${DOTNET_deps})
|
||||
IF(NOT dep MATCHES /obj/)
|
||||
IF(NOT dep MATCHES /obj/ AND NOT dep MATCHES /bin/)
|
||||
LIST(APPEND _DN_deps ${dep})
|
||||
ENDIF()
|
||||
ENDFOREACH()
|
||||
|
||||
GET_FILENAME_COMPONENT(_DN_abs_proj "${_DN_PROJECT}" ABSOLUTE)
|
||||
GET_FILENAME_COMPONENT(_DN_proj_dir "${_DN_PROJECT}" DIRECTORY)
|
||||
GET_FILENAME_COMPONENT(_DN_projname "${DOTNET_PROJECT}" NAME)
|
||||
STRING(REGEX REPLACE "\\.[^.]*$" "" _DN_projname_noext ${_DN_projname})
|
||||
|
||||
IF(_DN_RELEASE)
|
||||
SET(_DN_CONFIG Release)
|
||||
|
|
@ -186,10 +203,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments)
|
|||
ENDIF()
|
||||
|
||||
IF(NOT _DN_CONFIG)
|
||||
SET(_DN_CONFIG $<CONFIG>)
|
||||
IF(_DN_CONFIG STREQUAL "RelWithDebInfo" OR _DN_CONFIG STREQUAL "RelMinSize" OR NOT _DN_CONFIG)
|
||||
SET(_DN_CONFIG "Release")
|
||||
ENDIF()
|
||||
SET(_DN_CONFIG Release)
|
||||
ENDIF()
|
||||
|
||||
# If platform is not specified, do not pass the Platform property.
|
||||
|
|
@ -217,7 +231,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments)
|
|||
# Later we then copy the outputs to the destination.
|
||||
|
||||
IF(NOT _DN_OUTPUT_PATH)
|
||||
SET(_DN_OUTPUT_PATH "bin")
|
||||
SET(_DN_OUTPUT_PATH ${_DN_projname_noext})
|
||||
ENDIF()
|
||||
|
||||
GET_FILENAME_COMPONENT(_DN_OUTPUT_PATH ${CMAKE_CURRENT_BINARY_DIR}/${_DN_OUTPUT_PATH} ABSOLUTE)
|
||||
|
|
@ -295,14 +309,14 @@ ENDMACRO()
|
|||
MACRO(DOTNET_BUILD_COMMANDS)
|
||||
IF(${DOTNET_IS_MSBUILD})
|
||||
SET(build_dotnet_cmds
|
||||
COMMAND ${CMAKE_COMMAND} -E echo "=======> Building msbuild project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]"
|
||||
COMMAND ${NUGET_EXE} restore ${DOTNET_PROJPATH} -PackagesDirectory packages
|
||||
COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Clean /p:Configuration="${DOTNET_CONFIG}"
|
||||
COMMAND ${CMAKE_COMMAND} -E echo "======= Building msbuild project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]"
|
||||
COMMAND ${NUGET_EXE} restore -Force ${DOTNET_PROJPATH}
|
||||
COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Clean ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}"
|
||||
COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Build ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}")
|
||||
SET(build_dotnet_type "msbuild")
|
||||
ELSE()
|
||||
SET(build_dotnet_cmds
|
||||
COMMAND ${CMAKE_COMMAND} -E echo "=======> Building .NET project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]"
|
||||
COMMAND ${CMAKE_COMMAND} -E echo "======= Building .NET project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]"
|
||||
COMMAND ${DOTNET_EXE} restore ${DOTNET_PROJPATH} ${DOTNET_IMPORT_PROPERTIES}
|
||||
COMMAND ${DOTNET_EXE} clean ${DOTNET_PROJPATH} ${DOTNET_BUILD_PROPERTIES}
|
||||
COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS})
|
||||
|
|
@ -310,21 +324,22 @@ MACRO(DOTNET_BUILD_COMMANDS)
|
|||
ENDIF()
|
||||
|
||||
# DOTNET_OUTPUTS refer to artifacts produced, that the BUILD_proj_name target depends on.
|
||||
SET(DOTNET_OUTPUTS "")
|
||||
SET(DOTNET_OUTPUTS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.buildtimestamp)
|
||||
LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E touch ${DOTNET_OUTPUTS})
|
||||
IF(NOT "${DOTNET_PACKAGES}" STREQUAL "")
|
||||
MESSAGE("-- Adding ${build_dotnet_type} project ${DOTNET_PROJPATH} (version ${DOTNET_PACKAGE_VERSION})")
|
||||
SET(_DN_OUTPUTS "")
|
||||
FOREACH(pkg ${DOTNET_PACKAGES})
|
||||
LIST(APPEND _DN_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.nupkg)
|
||||
LIST(APPEND DOTNET_OUTPUTS ${CMAKE_BINARY_DIR}/${pkg}.${DOTNET_PACKAGE_VERSION}.nupkg)
|
||||
|
||||
LIST(APPEND _DN_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.symbols.nupkg)
|
||||
LIST(APPEND DOTNET_OUTPUTS ${CMAKE_BINARY_DIR}/${pkg}.${DOTNET_PACKAGE_VERSION}.symbols.nupkg)
|
||||
ENDFOREACH()
|
||||
LIST(APPEND build_dotnet_cmds COMMAND ${DOTNET_EXE} pack --no-build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_PACK_OPTIONS})
|
||||
LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E copy ${_DN_OUTPUTS} ${CMAKE_BINARY_DIR})
|
||||
ELSE()
|
||||
|
||||
MESSAGE("-- Adding ${build_dotnet_type} project ${DOTNET_PROJPATH} (no nupkg)")
|
||||
SET(DOTNET_OUTPUTS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.buildtimestamp)
|
||||
LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E touch ${DOTNET_OUTPUTS})
|
||||
ENDIF()
|
||||
|
||||
ADD_CUSTOM_COMMAND(
|
||||
|
|
@ -358,17 +373,23 @@ FUNCTION(ADD_MSBUILD DOTNET_PROJECT)
|
|||
ENDFUNCTION()
|
||||
|
||||
FUNCTION(RUN_DOTNET DOTNET_PROJECT)
|
||||
DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}")
|
||||
DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN};NETCOREAPP")
|
||||
MESSAGE("-- Adding dotnet run project ${DOTNET_PROJECT}")
|
||||
FILE(MAKE_DIRECTORY ${DOTNET_OUTPUT_PATH})
|
||||
ADD_CUSTOM_COMMAND(
|
||||
OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp ${DOTNET_RUN_OUTPUT}
|
||||
DEPENDS ${DOTNET_deps}
|
||||
COMMAND ${DOTNET_EXE} run ${DOTNET_RUN_ARGUMENTS}
|
||||
COMMAND ${DOTNET_EXE} restore ${DOTNET_PROJPATH} ${DOTNET_IMPORT_PROPERTIES}
|
||||
COMMAND ${DOTNET_EXE} clean ${DOTNET_PROJPATH} ${DOTNET_BUILD_PROPERTIES}
|
||||
COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS}
|
||||
# XXX tfm
|
||||
COMMAND ${DOTNET_EXE} ${DOTNET_OUTPUT_PATH}/netcoreapp2.0/${DOTNET_PROJNAME}.dll ${DOTNET_RUN_ARGUMENTS}
|
||||
COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp
|
||||
WORKING_DIRECTORY ${DOTNET_PROJDIR})
|
||||
WORKING_DIRECTORY ${DOTNET_OUTPUT_PATH})
|
||||
ADD_CUSTOM_TARGET(
|
||||
RUN_${DOTNET_PROJNAME}
|
||||
DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp ${DOTNET_RUN_OUTPUT})
|
||||
ADD_DEPENDENCIES(RUN_${DOTNET_PROJNAME} BUILD_${DOTNET_PROJNAME})
|
||||
ADD_DOTNET_DEPENDENCY_TARGETS(RUN)
|
||||
ENDFUNCTION()
|
||||
|
||||
FUNCTION(TEST_DOTNET DOTNET_PROJECT)
|
||||
|
|
@ -382,20 +403,18 @@ FUNCTION(TEST_DOTNET DOTNET_PROJECT)
|
|||
|
||||
ADD_TEST(NAME ${DOTNET_PROJNAME}
|
||||
COMMAND ${DOTNET_EXE} test ${test_framework_args} --results-directory "${CMAKE_BINARY_DIR}" --logger trx ${DOTNET_RUN_ARGUMENTS}
|
||||
WORKING_DIRECTORY ${DOTNET_PROJDIR})
|
||||
WORKING_DIRECTORY ${DOTNET_OUTPUT_PATH})
|
||||
|
||||
ENDFUNCTION()
|
||||
|
||||
SET(DOTNET_LAST_SMOKETEST "")
|
||||
SET_PROPERTY(GLOBAL PROPERTY DOTNET_LAST_SMOKETEST "")
|
||||
|
||||
FUNCTION(SMOKETEST_DOTNET DOTNET_PROJECT)
|
||||
MESSAGE("-- Adding dotnet smoke test project ${DOTNET_PROJECT}")
|
||||
IF(WIN32)
|
||||
ADD_DOTNET(${DOTNET_PROJECT} "${ARGN}")
|
||||
# TODO should run on all targeted frameworks
|
||||
RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}" ARGUMENTS -f netcoreapp2.0)
|
||||
RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}")
|
||||
ELSE()
|
||||
ADD_DOTNET(${DOTNET_PROJECT} "${ARGN}" NETCOREAPP)
|
||||
RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}" ARGUMENTS -f netcoreapp2.0)
|
||||
RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}")
|
||||
ENDIF()
|
||||
|
||||
DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}")
|
||||
|
|
@ -404,11 +423,13 @@ FUNCTION(SMOKETEST_DOTNET DOTNET_PROJECT)
|
|||
ALL
|
||||
DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp)
|
||||
ADD_DOTNET_DEPENDENCY_TARGETS(SMOKETEST)
|
||||
IF(DOTNET_LAST_SMOKETEST)
|
||||
ADD_DEPENDENCIES(SMOKETEST_${DOTNET_PROJNAME} ${DOTNET_LAST_SMOKETEST})
|
||||
GET_PROPERTY(_dn_last_smoketest GLOBAL PROPERTY DOTNET_LAST_SMOKETEST)
|
||||
IF(_dn_last_smoketest)
|
||||
MESSAGE("${_dn_last_smoketest} -> SMOKETEST_${DOTNET_PROJNAME}")
|
||||
ADD_DEPENDENCIES(SMOKETEST_${DOTNET_PROJNAME} ${_dn_last_smoketest})
|
||||
ENDIF()
|
||||
# Chain the smoke tests together so they are executed sequentially
|
||||
SET(DOTNET_LAST_SMOKETEST SMOKETEST_${DOTNET_PROJNAME})
|
||||
SET_PROPERTY(GLOBAL PROPERTY DOTNET_LAST_SMOKETEST SMOKETEST_${DOTNET_PROJNAME})
|
||||
|
||||
ENDFUNCTION()
|
||||
|
||||
|
|
|
|||
|
|
@ -15,8 +15,8 @@
|
|||
<Description>.NET Interface to the Z3 Theorem Prover</Description>
|
||||
<AssemblyDescription>.NET Interface to the Z3 Theorem Prover</AssemblyDescription>
|
||||
|
||||
<Copyright>Copyright (C) 2006-2015 Microsoft Corporation</Copyright>
|
||||
<AssemblyCopyright>Copyright (C) 2006-2015 Microsoft Corporation</AssemblyCopyright>
|
||||
<Copyright>Copyright (C) 2006-2019 Microsoft Corporation</Copyright>
|
||||
<AssemblyCopyright>Copyright (C) 2006-2019 Microsoft Corporation</AssemblyCopyright>
|
||||
|
||||
<Company>Microsoft Corporation</Company>
|
||||
<AssemblyCompany>Microsoft Corporation</AssemblyCompany>
|
||||
|
|
@ -36,163 +36,19 @@
|
|||
<AssemblyOriginatorKeyFile> </AssemblyOriginatorKeyFile>
|
||||
<DelaySign>false</DelaySign>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
|
||||
<CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
|
||||
<CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
|
||||
<CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
|
||||
<CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
|
||||
<CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
|
||||
<CodeContractsRunCodeAnalysis>True</CodeContractsRunCodeAnalysis>
|
||||
<CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
|
||||
<CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
|
||||
<CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>
|
||||
<CodeContractsEnumObligations>False</CodeContractsEnumObligations>
|
||||
<CodeContractsPointerObligations>False</CodeContractsPointerObligations>
|
||||
<CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
|
||||
<CodeContractsInferRequires>True</CodeContractsInferRequires>
|
||||
<CodeContractsInferEnsures>False</CodeContractsInferEnsures>
|
||||
<CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
|
||||
<CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
|
||||
<CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
|
||||
<CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
|
||||
<CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
|
||||
<CodeContractsDisjunctiveRequires>True</CodeContractsDisjunctiveRequires>
|
||||
<CodeContractsRunInBackground>True</CodeContractsRunInBackground>
|
||||
<CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
|
||||
<CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
|
||||
<CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
|
||||
<CodeContractsCustomRewriterAssembly />
|
||||
<CodeContractsCustomRewriterClass />
|
||||
<CodeContractsLibPaths />
|
||||
<CodeContractsExtraRewriteOptions />
|
||||
<CodeContractsExtraAnalysisOptions />
|
||||
<CodeContractsBaseLineFile />
|
||||
<CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
|
||||
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
|
||||
<CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
|
||||
<CodeContractsAnalysisWarningLevel>2</CodeContractsAnalysisWarningLevel>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x64'">
|
||||
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
|
||||
<CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
|
||||
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
|
||||
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
|
||||
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
|
||||
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
|
||||
<CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
|
||||
<CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
|
||||
<CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
|
||||
<CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
|
||||
<CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
|
||||
<CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
|
||||
<CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
|
||||
<CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
|
||||
<CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
|
||||
<CodeContractsEnumObligations>False</CodeContractsEnumObligations>
|
||||
<CodeContractsPointerObligations>False</CodeContractsPointerObligations>
|
||||
<CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
|
||||
<CodeContractsInferRequires>False</CodeContractsInferRequires>
|
||||
<CodeContractsInferEnsures>False</CodeContractsInferEnsures>
|
||||
<CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
|
||||
<CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
|
||||
<CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
|
||||
<CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
|
||||
<CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
|
||||
<CodeContractsRunInBackground>True</CodeContractsRunInBackground>
|
||||
<CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
|
||||
<CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
|
||||
<CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
|
||||
<CodeContractsCustomRewriterAssembly />
|
||||
<CodeContractsCustomRewriterClass />
|
||||
<CodeContractsLibPaths />
|
||||
<CodeContractsExtraRewriteOptions />
|
||||
<CodeContractsExtraAnalysisOptions />
|
||||
<CodeContractsBaseLineFile />
|
||||
<CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
|
||||
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
|
||||
<CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
|
||||
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x64'">
|
||||
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
|
||||
<CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
|
||||
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
|
||||
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
|
||||
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
|
||||
<CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
|
||||
<CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
|
||||
<CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
|
||||
<CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
|
||||
<CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
|
||||
<CodeContractsRunCodeAnalysis>True</CodeContractsRunCodeAnalysis>
|
||||
<CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
|
||||
<CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
|
||||
<CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
|
||||
<CodeContractsEnumObligations>False</CodeContractsEnumObligations>
|
||||
<CodeContractsPointerObligations>False</CodeContractsPointerObligations>
|
||||
<CodeContractsRedundantAssumptions>True</CodeContractsRedundantAssumptions>
|
||||
<CodeContractsInferRequires>True</CodeContractsInferRequires>
|
||||
<CodeContractsInferEnsures>False</CodeContractsInferEnsures>
|
||||
<CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
|
||||
<CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
|
||||
<CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
|
||||
<CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
|
||||
<CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
|
||||
<CodeContractsRunInBackground>True</CodeContractsRunInBackground>
|
||||
<CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
|
||||
<CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
|
||||
<CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
|
||||
<CodeContractsCustomRewriterAssembly />
|
||||
<CodeContractsCustomRewriterClass />
|
||||
<CodeContractsLibPaths />
|
||||
<CodeContractsExtraRewriteOptions />
|
||||
<CodeContractsExtraAnalysisOptions>-repro</CodeContractsExtraAnalysisOptions>
|
||||
<CodeContractsBaseLineFile />
|
||||
<CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
|
||||
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
|
||||
<CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
|
||||
<CodeContractsAnalysisWarningLevel>2</CodeContractsAnalysisWarningLevel>
|
||||
</PropertyGroup>
|
||||
|
||||
<PropertyGroup Condition="'$(Configuration)' == 'Release_delaysign'">
|
||||
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
|
||||
<CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
|
||||
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
|
||||
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
|
||||
<CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
|
||||
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
|
||||
<DefineConstants>DELAYSIGN</DefineConstants>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition=" '$(Configuration)' == 'external' ">
|
||||
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
|
||||
<CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
|
||||
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
|
||||
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
|
||||
<CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
|
||||
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
|
||||
<CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Platform)' == 'x86'">
|
||||
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
|
||||
<CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
|
||||
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
|
||||
<CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
|
||||
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
|
||||
</PropertyGroup>
|
||||
|
||||
<!-- Build properties -->
|
||||
<PropertyGroup>
|
||||
<!-- Add net40;net35 only if the appropriate SDKs are installed. -->
|
||||
<!-- Also, in xplat builds, netfx TFMs are not available. -->
|
||||
<!-- In *nix builds, netfx TFMs are not available. -->
|
||||
<TargetFrameworks>netstandard2.0;net461;net45</TargetFrameworks>
|
||||
<OutputTypeEx>library</OutputTypeEx>
|
||||
<AllowUnsafeBlocks>True</AllowUnsafeBlocks>
|
||||
<NoWarn>1701,1702</NoWarn>
|
||||
<Warn>4</Warn>
|
||||
<DefineConstants Condition="'$(TargetFramework)'=='net35'">FRAMEWORK_LT_4</DefineConstants>
|
||||
<GenerateDocumentationFile>true</GenerateDocumentationFile>
|
||||
<DocumentationFile>$(OutputPath)\Microsoft.Z3.xml</DocumentationFile>
|
||||
</PropertyGroup>
|
||||
|
|
@ -224,20 +80,11 @@ ${Z3_DOTNET_COMPILE_ITEMS}
|
|||
</Content>
|
||||
</ItemGroup>
|
||||
|
||||
<!-- Native binaries for x86, note the platform condition is set to "AnyCPU" -->
|
||||
<ItemGroup Condition="'$(Platform)' == 'AnyCPU'">
|
||||
<!-- Native binaries for x86; currently only Windows is supported. -->
|
||||
<ItemGroup Condition="'$(Platform)' == 'x86'">
|
||||
<Content Include="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/$(Configuration)/libz3.dll" Condition="Exists('${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/$(Configuration)/libz3.dll')">
|
||||
<PackagePath>runtimes\win-x86\native</PackagePath>
|
||||
</Content>
|
||||
<Content Include="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libz3.so" Condition="Exists('${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libz3.so')">
|
||||
<PackagePath>runtimes\linux-x86\native</PackagePath>
|
||||
</Content>
|
||||
</ItemGroup>
|
||||
|
||||
|
||||
<!-- NuGet package references -->
|
||||
<ItemGroup Condition="'$(TargetFramework)'=='net35'">
|
||||
<PackageReference Include="Code.Contract" Version="1.0.0"/>
|
||||
</ItemGroup>
|
||||
|
||||
</Project>
|
||||
|
|
|
|||
|
|
@ -1,15 +0,0 @@
|
|||
Z3 API for .NET Core
|
||||
|
||||
Z3's .NET API uses Code Contracts, which are not included in .NET Core. The
|
||||
enclosed file called DummyContracts.cs provides stubs for the Code Contracts
|
||||
functions, so that the API will compile, but not perform any contract
|
||||
checking. To build this using .NET core, run (in this directory):
|
||||
|
||||
dotnet restore
|
||||
dotnet build core.csproj -c Release
|
||||
|
||||
If you are building with the cmake system, you should first
|
||||
copy over files that are produced by the compiler into
|
||||
this directory. You need to copy over Native.cs and Enumeration.cs
|
||||
|
||||
-- good luck!
|
||||
|
|
@ -1,18 +0,0 @@
|
|||
<Project Sdk="Microsoft.NET.Sdk">
|
||||
|
||||
<PropertyGroup>
|
||||
<TargetFramework>netcoreapp1.0</TargetFramework>
|
||||
<DefineConstants>$(DefineConstants);DOTNET_CORE</DefineConstants>
|
||||
<DebugType>portable</DebugType>
|
||||
<AssemblyName>Microsoft.Z3</AssemblyName>
|
||||
<OutputType>Library</OutputType>
|
||||
<PackageId>core</PackageId>
|
||||
<PackageTargetFallback>$(PackageTargetFallback);dnxcore50</PackageTargetFallback>
|
||||
<RuntimeFrameworkVersion>1.0.4</RuntimeFrameworkVersion>
|
||||
</PropertyGroup>
|
||||
|
||||
<ItemGroup>
|
||||
<Compile Include="..\*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" />
|
||||
</ItemGroup>
|
||||
|
||||
</Project>
|
||||
|
|
@ -1,10 +0,0 @@
|
|||
The default Z3 bindings for .NET are built for the .NET framework version 4.
|
||||
Should the need arise, it is also possible to build them for .NET 3.5; the
|
||||
instructions are as follows:
|
||||
|
||||
In the project properties of Microsoft.Z3.csproj:
|
||||
- Under 'Application': Change Target framework to .NET Framework 3.5
|
||||
- Under 'Build': Add FRAMEWORK_LT_4 to the conditional compilation symbols
|
||||
- Remove the reference to System.Numerics
|
||||
- Install the NuGet Package "Microsoft Code Contracts for Net3.5":
|
||||
In the Package Manager Console enter Install-Package Code.Contract
|
||||
Loading…
Reference in a new issue