mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	Merge branch 'pypy-fix' of https://github.com/zardus/z3 into zardus-76
# Conflicts: # scripts/mk_util.py
This commit is contained in:
		
						commit
						eb0cdc42d1
					
				
					 1 changed files with 34 additions and 1 deletions
				
			
		| 
						 | 
				
			
			@ -180,6 +180,8 @@ def exec_cmd(cmd):
 | 
			
		|||
    except:
 | 
			
		||||
        # Failed to create process
 | 
			
		||||
        return 1
 | 
			
		||||
    finally:
 | 
			
		||||
        null.close()
 | 
			
		||||
 | 
			
		||||
# rm -f fname
 | 
			
		||||
def rmf(fname):
 | 
			
		||||
| 
						 | 
				
			
			@ -353,6 +355,7 @@ def check_java():
 | 
			
		|||
                    q = os.path.dirname(libdir)
 | 
			
		||||
                    if cdirs.count(q) == 0:
 | 
			
		||||
                        cdirs.append(q)
 | 
			
		||||
        t.close()
 | 
			
		||||
 | 
			
		||||
        # ... plus some heuristic ones.
 | 
			
		||||
        extra_dirs = []
 | 
			
		||||
| 
						 | 
				
			
			@ -419,6 +422,9 @@ def find_ml_lib():
 | 
			
		|||
        t.commit()
 | 
			
		||||
    except:
 | 
			
		||||
        raise MKException('Failed to find Ocaml library; please set OCAML_LIB')
 | 
			
		||||
    finally:
 | 
			
		||||
        null.close()
 | 
			
		||||
 | 
			
		||||
    t = open('output', 'r')
 | 
			
		||||
    for line in t:
 | 
			
		||||
        OCAML_LIB = line[:-1]
 | 
			
		||||
| 
						 | 
				
			
			@ -477,6 +483,7 @@ def is_cr_lf(fname):
 | 
			
		|||
    # Check whether text files use cr/lf
 | 
			
		||||
    f = open(fname, 'r')
 | 
			
		||||
    line = f.readline()
 | 
			
		||||
    f.close()
 | 
			
		||||
    sz = len(line)
 | 
			
		||||
    return sz >= 2 and line[sz-2] == '\r' and line[sz-1] == '\n'
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -672,6 +679,7 @@ def extract_c_includes(fname):
 | 
			
		|||
        elif not system_inc_pat.match(line) and non_std_inc_pat.match(line):
 | 
			
		||||
            raise MKException("Invalid #include directive at '%s':%s" % (fname, line))
 | 
			
		||||
        linenum = linenum + 1
 | 
			
		||||
    f.close()
 | 
			
		||||
    return result
 | 
			
		||||
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -1958,6 +1966,8 @@ def mk_config():
 | 
			
		|||
                print('OCaml Native:   %s' % OCAMLOPT)
 | 
			
		||||
                print('OCaml Library:  %s' % OCAML_LIB)
 | 
			
		||||
 | 
			
		||||
    config.close()
 | 
			
		||||
 | 
			
		||||
def mk_install(out):
 | 
			
		||||
    out.write('install: ')
 | 
			
		||||
    for c in get_components():
 | 
			
		||||
| 
						 | 
				
			
			@ -2031,6 +2041,7 @@ def mk_makefile():
 | 
			
		|||
    if not IS_WINDOWS:
 | 
			
		||||
        mk_install(out)
 | 
			
		||||
        mk_uninstall(out)
 | 
			
		||||
    out.close()
 | 
			
		||||
    # Finalize
 | 
			
		||||
    if VERBOSE:
 | 
			
		||||
        print("Makefile was successfully generated.")
 | 
			
		||||
| 
						 | 
				
			
			@ -2144,6 +2155,7 @@ def def_module_params(module_name, export, params, class_name=None, description=
 | 
			
		|||
                      (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param)))
 | 
			
		||||
    out.write('};\n')
 | 
			
		||||
    out.write('#endif\n')
 | 
			
		||||
    out.close()
 | 
			
		||||
    if is_verbose():
 | 
			
		||||
        print("Generated '%s'" % hpp)
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -2186,6 +2198,8 @@ def mk_pat_db():
 | 
			
		|||
    for line in fin:
 | 
			
		||||
        fout.write('"%s\\n"\n' % line.strip('\n'))
 | 
			
		||||
    fout.write(';\n')
 | 
			
		||||
    fin.close()
 | 
			
		||||
    fout.close()
 | 
			
		||||
    if VERBOSE:
 | 
			
		||||
        print("Generated '%s'" % os.path.join(c.src_dir, 'database.h'))
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -2211,6 +2225,7 @@ def mk_version_dot_h(major, minor, build, revision):
 | 
			
		|||
    fout.write('#define Z3_MINOR_VERSION   %s\n' % minor)
 | 
			
		||||
    fout.write('#define Z3_BUILD_NUMBER    %s\n' % build)
 | 
			
		||||
    fout.write('#define Z3_REVISION_NUMBER %s\n' % revision)
 | 
			
		||||
    fout.close()
 | 
			
		||||
    if VERBOSE:
 | 
			
		||||
        print("Generated '%s'" % os.path.join(c.src_dir, 'version.h'))
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -2302,6 +2317,7 @@ def mk_install_tactic_cpp(cnames, path):
 | 
			
		|||
                        exec(line.strip('\n '), globals())
 | 
			
		||||
                    except:
 | 
			
		||||
                        raise MKException("Failed processing ADD_PROBE command at '%s'\n%s" % (fullname, line))
 | 
			
		||||
            fin.close()
 | 
			
		||||
    # First pass will just generate the tactic factories
 | 
			
		||||
    idx = 0
 | 
			
		||||
    for data in ADD_TACTIC_DATA:
 | 
			
		||||
| 
						 | 
				
			
			@ -2317,6 +2333,7 @@ def mk_install_tactic_cpp(cnames, path):
 | 
			
		|||
    for data in ADD_PROBE_DATA:
 | 
			
		||||
        fout.write('  ADD_PROBE("%s", "%s", %s);\n' % data)
 | 
			
		||||
    fout.write('}\n')
 | 
			
		||||
    fout.close()
 | 
			
		||||
    if VERBOSE:
 | 
			
		||||
        print("Generated '%s'" % fullname)
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -2369,6 +2386,7 @@ def mk_mem_initializer_cpp(cnames, path):
 | 
			
		|||
                        added_include = True
 | 
			
		||||
                        fout.write('#include"%s"\n' % h_file)
 | 
			
		||||
                    finalizer_cmds.append(m.group(1))
 | 
			
		||||
            fin.close()
 | 
			
		||||
    initializer_cmds.sort(key=lambda tup: tup[1])
 | 
			
		||||
    fout.write('void mem_initialize() {\n')
 | 
			
		||||
    for (cmd, prio) in initializer_cmds:
 | 
			
		||||
| 
						 | 
				
			
			@ -2380,6 +2398,7 @@ def mk_mem_initializer_cpp(cnames, path):
 | 
			
		|||
        fout.write(cmd)
 | 
			
		||||
        fout.write('\n')
 | 
			
		||||
    fout.write('}\n')
 | 
			
		||||
    fout.close()
 | 
			
		||||
    if VERBOSE:
 | 
			
		||||
        print("Generated '%s'" % fullname)
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -2429,6 +2448,7 @@ def mk_gparams_register_modules(cnames, path):
 | 
			
		|||
                m = reg_mod_descr_pat.match(line)
 | 
			
		||||
                if m:
 | 
			
		||||
                    mod_descrs.append((m.group(1), m.group(2)))
 | 
			
		||||
            fin.close()
 | 
			
		||||
    fout.write('void gparams_register_modules() {\n')
 | 
			
		||||
    for code in cmds:
 | 
			
		||||
        fout.write('{ param_descrs d; %s(d); gparams::register_global(d); }\n' % code)
 | 
			
		||||
| 
						 | 
				
			
			@ -2437,6 +2457,7 @@ def mk_gparams_register_modules(cnames, path):
 | 
			
		|||
    for (mod, descr) in mod_descrs:
 | 
			
		||||
        fout.write('gparams::register_module_descr("%s", "%s");\n' % (mod, descr))
 | 
			
		||||
    fout.write('}\n')
 | 
			
		||||
    fout.close()
 | 
			
		||||
    if VERBOSE:
 | 
			
		||||
        print("Generated '%s'" % fullname)
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -2470,6 +2491,8 @@ def mk_def_file(c):
 | 
			
		|||
                        fout.write('\t%s @%s\n' % (f, num))
 | 
			
		||||
                    i = i + 1
 | 
			
		||||
                num = num + 1
 | 
			
		||||
        api.close()
 | 
			
		||||
    fout.close()
 | 
			
		||||
    if VERBOSE:
 | 
			
		||||
        print("Generated '%s'" % defname)
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -2604,6 +2627,8 @@ def mk_z3consts_py(api_files):
 | 
			
		|||
                    decls[words[1]] = idx
 | 
			
		||||
                    idx = idx + 1
 | 
			
		||||
            linenum = linenum + 1
 | 
			
		||||
        api.close()
 | 
			
		||||
    z3consts.close()
 | 
			
		||||
    if VERBOSE:
 | 
			
		||||
        print("Generated '%s'" % os.path.join(Z3PY_SRC_DIR, 'z3consts.py'))
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -2689,7 +2714,9 @@ def mk_z3consts_dotnet(api_files):
 | 
			
		|||
                    decls[words[1]] = idx
 | 
			
		||||
                    idx = idx + 1
 | 
			
		||||
            linenum = linenum + 1
 | 
			
		||||
    z3consts.write('}\n')
 | 
			
		||||
        api.close()
 | 
			
		||||
    z3consts.write('}\n');
 | 
			
		||||
    z3consts.close()
 | 
			
		||||
    if VERBOSE:
 | 
			
		||||
        print("Generated '%s'" % os.path.join(dotnet.src_dir, 'Enumerations.cs'))
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -2796,6 +2823,7 @@ def mk_z3consts_java(api_files):
 | 
			
		|||
                    decls[words[1]] = idx
 | 
			
		||||
                    idx = idx + 1
 | 
			
		||||
            linenum = linenum + 1
 | 
			
		||||
        api.close()
 | 
			
		||||
    if VERBOSE:
 | 
			
		||||
        print("Generated '%s'" % ('%s' % gendir))
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -2891,6 +2919,8 @@ def mk_z3consts_ml(api_files):
 | 
			
		|||
                    decls[words[1]] = idx
 | 
			
		||||
                    idx = idx + 1
 | 
			
		||||
            linenum = linenum + 1
 | 
			
		||||
        api.close()
 | 
			
		||||
    efile.close()
 | 
			
		||||
    if VERBOSE:
 | 
			
		||||
        print ('Generated "%s/z3enums.ml"' % ('%s' % gendir))
 | 
			
		||||
    efile  = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w')
 | 
			
		||||
| 
						 | 
				
			
			@ -2961,6 +2991,8 @@ def mk_z3consts_ml(api_files):
 | 
			
		|||
                    decls[words[1]] = idx
 | 
			
		||||
                    idx = idx + 1
 | 
			
		||||
            linenum = linenum + 1
 | 
			
		||||
        api.close()
 | 
			
		||||
    efile.close()
 | 
			
		||||
    if VERBOSE:
 | 
			
		||||
        print ('Generated "%s/z3enums.mli"' % ('%s' % gendir))
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			@ -3097,6 +3129,7 @@ def mk_vs_proj(name, components):
 | 
			
		|||
    f.write('  <ImportGroup Label="ExtensionTargets">\n')
 | 
			
		||||
    f.write('  </ImportGroup>\n')
 | 
			
		||||
    f.write('</Project>\n')
 | 
			
		||||
    f.close()
 | 
			
		||||
    if is_verbose():
 | 
			
		||||
        print("Generated '%s'" % proj_name)
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue