mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

Merge branch 'buildsystem_cleanup' of https://github.com/daniel-j-h/z3 into daniel-j-h-buildsystem_cleanup

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-19 15:18:13 +01:00
parent 6749c19ab1 ce9036c300
commit b1fcdadd55
2 changed files with 62 additions and 62 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

54
scripts/mk_util.py
View file

@ -282,7 +282,7 @@ def check_java():
if is_verbose():
print("Finding javac ...")
if JDK_HOME != None:
if JDK_HOME is not None:
if IS_WINDOWS:
JAVAC = os.path.join(JDK_HOME, 'bin', 'javac.exe')
else:
@ -292,7 +292,7 @@ def check_java():
raise MKException("Failed to detect javac at '%s/bin'; the environment variable JDK_HOME is probably set to the wrong path." % os.path.join(JDK_HOME))
else:
# Search for javac in the path.
ind = 'javac';
ind = 'javac'
if IS_WINDOWS:
ind = ind + '.exe'
paths = os.getenv('PATH', None)
@ -304,7 +304,7 @@ def check_java():
JAVAC = cmb
break
if JAVAC == None:
if JAVAC is None:
raise MKException('No java compiler in the path, please adjust your PATH or set JDK_HOME to the location of the JDK.')
if is_verbose():
@ -339,7 +339,7 @@ def check_java():
if is_verbose():
print("Finding jni.h...")
if JNI_HOME != None:
if JNI_HOME is not None:
if not os.path.exists(os.path.join(JNI_HOME, 'jni.h')):
raise MKException("Failed to detect jni.h '%s'; the environment variable JNI_HOME is probably set to the wrong path." % os.path.join(JNI_HOME))
else:
@ -371,10 +371,10 @@ def check_java():
for dir in cdirs:
q = find_jni_h(dir)
if q != False:
if q is not False:
JNI_HOME = q
if JNI_HOME == None:
if JNI_HOME is None:
raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.")
def check_ml():
@ -437,12 +437,12 @@ def is64():
def check_ar():
if is_verbose():
print("Testing ar...")
if which('ar')== None:
if which('ar') is None:
raise MKException('ar (archive tool) was not found')
def find_cxx_compiler():
global CXX, CXX_COMPILERS
if CXX != None:
if CXX is not None:
if test_cxx_compiler(CXX):
return CXX
for cxx in CXX_COMPILERS:
@ -453,7 +453,7 @@ def find_cxx_compiler():
def find_c_compiler():
global CC, C_COMPILERS
if CC != None:
if CC is not None:
if test_c_compiler(CC):
return CC
for c in C_COMPILERS:
@ -805,7 +805,7 @@ class Component:
global BUILD_DIR, SRC_DIR, REV_BUILD_DIR
if name in _ComponentNames:
raise MKException("Component '%s' was already defined." % name)
if path == None:
if path is None:
path = name
self.name = name
path = norm_path(path)
@ -1019,7 +1019,7 @@ def sort_components(cnames):
class ExeComponent(Component):
def __init__(self, name, exe_name, path, deps, install):
Component.__init__(self, name, path, deps)
if exe_name == None:
if exe_name is None:
exe_name = name
self.exe_name = exe_name
self.install = install
@ -1113,7 +1113,7 @@ def get_so_ext():
class DLLComponent(Component):
def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static):
Component.__init__(self, name, path, deps)
if dll_name == None:
if dll_name is None:
dll_name = name
self.dll_name = dll_name
self.export_files = export_files
@ -1147,7 +1147,7 @@ class DLLComponent(Component):
out.write(' ')
out.write(obj)
for dep in deps:
if not dep in self.reexports:
if dep not in self.reexports:
c_dep = get_component(dep)
out.write(' ' + c_dep.get_link_name())
out.write('\n')
@ -1156,7 +1156,7 @@ class DLLComponent(Component):
out.write(' ')
out.write(obj)
for dep in deps:
if not dep in self.reexports:
if dep not in self.reexports:
c_dep = get_component(dep)
out.write(' ' + c_dep.get_link_name())
out.write(' ' + FOCI2LIB)
@ -1249,9 +1249,9 @@ class DLLComponent(Component):
class DotNetDLLComponent(Component):
def __init__(self, name, dll_name, path, deps, assembly_info_dir):
Component.__init__(self, name, path, deps)
if dll_name == None:
if dll_name is None:
dll_name = name
if assembly_info_dir == None:
if assembly_info_dir is None:
assembly_info_dir = "."
self.dll_name = dll_name
self.assembly_info_dir = assembly_info_dir
@ -1315,7 +1315,7 @@ class DotNetDLLComponent(Component):
class JavaDLLComponent(Component):
def __init__(self, name, dll_name, package_name, manifest_file, path, deps):
Component.__init__(self, name, path, deps)
if dll_name == None:
if dll_name is None:
dll_name = name
self.dll_name = dll_name
self.package_name = package_name
@ -1406,7 +1406,7 @@ class JavaDLLComponent(Component):
class MLComponent(Component):
def __init__(self, name, lib_name, path, deps):
Component.__init__(self, name, path, deps)
if lib_name == None:
if lib_name is None:
lib_name = name
self.lib_name = lib_name
@ -1473,7 +1473,7 @@ class MLComponent(Component):
out.write('%s: %s %s\n' %
(os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)'),
os.path.join(sub_dir, 'z3native_stubs.c'),
get_component(Z3_DLL_COMPONENT).dll_name+'$(SO_EXT)'));
get_component(Z3_DLL_COMPONENT).dll_name+'$(SO_EXT)'))
out.write('\t$(CC) $(CXXFLAGS_OCAML) -I %s -I %s %s $(CXX_OUT_FLAG)%s$(OBJ_EXT)\n' %
(OCAML_LIB, api_src, os.path.join(sub_dir, 'z3native_stubs.c'), os.path.join(sub_dir, 'z3native_stubs')))
@ -2107,7 +2107,7 @@ def to_c_method(s):
def def_module_params(module_name, export, params, class_name=None, description=None):
pyg = get_curr_pyg()
dirname = os.path.split(get_curr_pyg())[0]
if class_name == None:
if class_name is None:
class_name = '%s_params' % module_name
hpp = os.path.join(dirname, '%s.hpp' % class_name)
out = open(hpp, 'w')
@ -2133,7 +2133,7 @@ def def_module_params(module_name, export, params, class_name=None, description=
if export:
out.write(' /*\n')
out.write(" REG_MODULE_PARAMS('%s', '%s::collect_param_descrs')\n" % (module_name, class_name))
if description != None:
if description is not None:
out.write(" REG_MODULE_DESCRIPTION('%s', '%s')\n" % (module_name, description))
out.write(' */\n')
# Generated accessors
@ -2197,7 +2197,7 @@ def update_version():
minor = VER_MINOR
build = VER_BUILD
revision = VER_REVISION
if major == None or minor == None or build == None or revision == None:
if major is None or minor is None or build is None or revision is None:
raise MKException("set_version(major, minor, build, revision) must be used before invoking update_version()")
if not ONLY_MAKEFILES:
mk_version_dot_h(major, minor, build, revision)
@ -2533,7 +2533,7 @@ def mk_bindings(api_files):
# Extract enumeration types from API files, and add python definitions.
def mk_z3consts_py(api_files):
if Z3PY_SRC_DIR == None:
if Z3PY_SRC_DIR is None:
raise MKException("You must invoke set_z3py_dir(path):")
blank_pat = re.compile("^ *$")
@ -2627,7 +2627,7 @@ def mk_z3consts_dotnet(api_files):
z3consts.write('using System;\n\n'
'#pragma warning disable 1591\n\n'
'namespace Microsoft.Z3\n'
'{\n');
'{\n')
for api_file in api_files:
api_file_c = dotnet.find_file(api_file, dotnet.name)
@ -2691,7 +2691,7 @@ def mk_z3consts_dotnet(api_files):
decls[words[1]] = idx
idx = idx + 1
linenum = linenum + 1
z3consts.write('}\n');
z3consts.write('}\n')
if VERBOSE:
print("Generated '%s'" % os.path.join(dotnet.src_dir, 'Enumerations.cs'))
@ -2759,7 +2759,7 @@ def mk_z3consts_java(api_files):
if name not in DeprecatedEnums:
efile = open('%s.java' % os.path.join(gendir, name), 'w')
efile.write('/**\n * Automatically generated file\n **/\n\n')
efile.write('package %s.enumerations;\n\n' % java.package_name);
efile.write('package %s.enumerations;\n\n' % java.package_name)
efile.write('/**\n')
efile.write(' * %s\n' % name)
@ -2770,7 +2770,7 @@ def mk_z3consts_java(api_files):
for k in decls:
i = decls[k]
if first:
first = False
first = False
else:
efile.write(',\n')
efile.write(' %s (%s)' % (k, i))

70
scripts/update_api.py
View file

@ -217,16 +217,16 @@ def type2ml(ty):
return Type2ML[ty]
def _in(ty):
return (IN, ty);
return (IN, ty)
def _in_array(sz, ty):
return (IN_ARRAY, ty, sz);
return (IN_ARRAY, ty, sz)
def _out(ty):
return (OUT, ty);
return (OUT, ty)
def _out_array(sz, ty):
return (OUT_ARRAY, ty, sz, sz);
return (OUT_ARRAY, ty, sz, sz)
# cap contains the position of the argument that stores the capacity of the array
# sz contains the position of the output argument that stores the (real) size of the array
@ -234,7 +234,7 @@ def _out_array2(cap, sz, ty):
return (OUT_ARRAY, ty, cap, sz)
def _inout_array(sz, ty):
return (INOUT_ARRAY, ty, sz, sz);
return (INOUT_ARRAY, ty, sz, sz)
def _out_managed_array(sz,ty):
return (OUT_MANAGED_ARRAY, ty, 0, sz)
@ -314,7 +314,7 @@ def param2javaw(p):
else:
return "jlongArray"
elif k == OUT_MANAGED_ARRAY:
return "jlong";
return "jlong"
else:
return type2javaw(param_type(p))
@ -336,7 +336,7 @@ def param2ml(p):
elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
return "%s array" % type2ml(param_type(p))
elif k == OUT_MANAGED_ARRAY:
return "%s array" % type2ml(param_type(p));
return "%s array" % type2ml(param_type(p))
else:
return type2ml(param_type(p))
@ -422,14 +422,14 @@ def mk_dotnet():
dotnet.write('using System.Collections.Generic;\n')
dotnet.write('using System.Text;\n')
dotnet.write('using System.Runtime.InteropServices;\n\n')
dotnet.write('#pragma warning disable 1591\n\n');
dotnet.write('#pragma warning disable 1591\n\n')
dotnet.write('namespace Microsoft.Z3\n')
dotnet.write('{\n')
for k in Type2Str:
v = Type2Str[k]
if is_obj(k):
dotnet.write(' using %s = System.IntPtr;\n' % v)
dotnet.write('\n');
dotnet.write('\n')
dotnet.write(' public class Native\n')
dotnet.write(' {\n\n')
dotnet.write(' [UnmanagedFunctionPointer(CallingConvention.Cdecl)]\n')
@ -437,7 +437,7 @@ def mk_dotnet():
dotnet.write(' public unsafe class LIB\n')
dotnet.write(' {\n')
dotnet.write(' const string Z3_DLL_NAME = \"libz3.dll\";\n'
' \n');
' \n')
dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n')
dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n')
for name, result, params in _dotnet_decls:
@ -448,7 +448,7 @@ def mk_dotnet():
else:
dotnet.write('public extern static %s %s(' % (type2dotnet(result), name))
first = True
i = 0;
i = 0
for param in params:
if first:
first = False
@ -480,7 +480,7 @@ def mk_dotnet_wrappers():
else:
dotnet.write(' public static %s %s(' % (type2dotnet(result), name))
first = True
i = 0;
i = 0
for param in params:
if first:
first = False
@ -491,9 +491,9 @@ def mk_dotnet_wrappers():
dotnet.write(') {\n')
dotnet.write(' ')
if result == STRING:
dotnet.write('IntPtr r = ');
dotnet.write('IntPtr r = ')
elif result != VOID:
dotnet.write('%s r = ' % type2dotnet(result));
dotnet.write('%s r = ' % type2dotnet(result))
dotnet.write('LIB.%s(' % (name))
first = True
i = 0
@ -504,14 +504,14 @@ def mk_dotnet_wrappers():
dotnet.write(', ')
if param_kind(param) == OUT:
if param_type(param) == STRING:
dotnet.write('out ');
dotnet.write('out ')
else:
dotnet.write('ref ')
elif param_kind(param) == OUT_MANAGED_ARRAY:
dotnet.write('out ');
dotnet.write('out ')
dotnet.write('a%d' % i)
i = i + 1
dotnet.write(');\n');
dotnet.write(');\n')
if name not in Unwrapped:
if name in NULLWrapped:
dotnet.write(" if (r == IntPtr.Zero)\n")
@ -578,7 +578,7 @@ def mk_java():
for name, result, params in _dotnet_decls:
java_native.write(' protected static native %s INTERNAL%s(' % (type2java(result), java_method_name(name)))
first = True
i = 0;
i = 0
for param in params:
if first:
first = False
@ -592,7 +592,7 @@ def mk_java():
for name, result, params in _dotnet_decls:
java_native.write(' public static %s %s(' % (type2java(result), java_method_name(name)))
first = True
i = 0;
i = 0
for param in params:
if first:
first = False
@ -610,7 +610,7 @@ def mk_java():
java_native.write('%s res = ' % type2java(result))
java_native.write('INTERNAL%s(' % (java_method_name(name)))
first = True
i = 0;
i = 0
for param in params:
if first:
first = False
@ -698,7 +698,7 @@ def mk_java():
java_wrapper.write('')
for name, result, params in _dotnet_decls:
java_wrapper.write('DLL_VIS JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name)))
i = 0;
i = 0
for param in params:
java_wrapper.write(', ')
java_wrapper.write('%s a%d' % (param2javaw(param), i))
@ -804,10 +804,10 @@ def mk_log_header(file, name, params):
i = 0
for p in params:
if i > 0:
file.write(", ");
file.write(", ")
file.write("%s a%s" % (param2str(p), i))
i = i + 1
file.write(")");
file.write(")")
def log_param(p):
kind = param_kind(p)
@ -964,7 +964,7 @@ def def_API(name, result, params):
log_c.write(" I(a%s);\n" % i)
exe_c.write("in.get_bool(%s)" % i)
elif ty == PRINT_MODE or ty == ERROR_CODE:
log_c.write(" U(static_cast<unsigned>(a%s));\n" % i);
log_c.write(" U(static_cast<unsigned>(a%s));\n" % i)
exe_c.write("static_cast<%s>(in.get_uint(%s))" % (type2str(ty), i))
else:
error("unsupported parameter for %s, %s" % (name, p))
@ -1081,10 +1081,10 @@ def ml_method_name(name):
return name[3:] # Remove Z3_
def is_out_param(p):
if param_kind(p) == OUT or param_kind(p) == INOUT or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT_MANAGED_ARRAY:
return True
else:
return False
if param_kind(p) == OUT or param_kind(p) == INOUT or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT_MANAGED_ARRAY:
return True
else:
return False
def outparams(params):
op = []
@ -1169,7 +1169,7 @@ def mk_ml():
ml_native.write('(** The native (raw) interface to the dynamic Z3 library. *)\n\n')
ml_i.write('(* Automatically generated file *)\n\n')
ml_i.write('(** The native (raw) interface to the dynamic Z3 library. *)\n\n')
ml_i.write('(**/**)\n\n');
ml_i.write('(**/**)\n\n')
ml_native.write('open Z3enums\n\n')
ml_native.write('(**/**)\n')
ml_native.write('type ptr\n')
@ -1232,7 +1232,7 @@ def mk_ml():
ml_native.write(' = "n_%s"\n' % ml_method_name(name))
ml_native.write('\n')
ml_native.write(' end\n\n')
ml_i.write('\n(**/**)\n');
ml_i.write('\n(**/**)\n')
# Exception wrappers
for name, result, params in _dotnet_decls:
@ -1241,11 +1241,11 @@ def mk_ml():
ml_native.write(' let %s ' % ml_method_name(name))
first = True
i = 0;
i = 0
for p in params:
if is_in_param(p):
if first:
first = False;
first = False
else:
ml_native.write(' ')
ml_native.write('a%d' % i)
@ -1262,7 +1262,7 @@ def mk_ml():
if len(ip) == 0:
ml_native.write(' ()')
first = True
i = 0;
i = 0
for p in params:
if is_in_param(p):
ml_native.write(' a%d' % i)
@ -1476,7 +1476,7 @@ def mk_ml():
if len(op) > 0:
if result != VOID:
ml_wrapper.write(' %s\n' % ml_set_wrap(result, "res_val", "z3_result"))
i = 0;
i = 0
for p in params:
if param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY:
ml_wrapper.write(' _a%s_val = caml_alloc(_a%s, 0);\n' % (i, param_array_capacity_pos(p)))
@ -1499,7 +1499,7 @@ def mk_ml():
for p in params:
if is_out_param(p):
ml_wrapper.write(' Store_field(result, %s, _a%s_val);\n' % (j, i))
j = j + 1;
j = j + 1
i = i + 1
# local array cleanup