mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

Minor adjustments after rebase

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-19 17:35:19 +00:00
parent c9fa77cc70
commit ed0fa93245
2 changed files with 5 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

2
examples/ml/ml_example.ml
View file

@ -190,7 +190,7 @@ let basic_tests ( ctx : context ) =
(* Error handling test. *) (* Error handling test. *)
try ( try (
let i = Integer.mk_numeral_s ctx "1/2" in let i = Integer.mk_numeral_s ctx "1/2" in
raise (TestFailedException "") (* unreachable *) raise (TestFailedException (to_string i)) (* unreachable *)
) )
with Z3native.Exception(_) -> ( with Z3native.Exception(_) -> (
Printf.printf "Exception caught, OK.\n" Printf.printf "Exception caught, OK.\n"

15
scripts/mk_util.py
View file

@ -357,14 +357,13 @@ def check_ml():
rmf('hello.cmo') rmf('hello.cmo')
rmf('hello.cmx') rmf('hello.cmx')
rmf('a.out') rmf('a.out')
rmf('hello.o')
find_ml_lib() find_ml_lib()
find_ocaml_find() find_ocaml_find()
def find_ocaml_find(): def find_ocaml_find():
global OCAMLFIND global OCAMLFIND
if is_verbose(): if is_verbose():
print ('Testing %s...' % OCAMLFIND) print ("Testing %s..." % OCAMLFIND)
r = exec_cmd([OCAMLFIND, 'printconf']) r = exec_cmd([OCAMLFIND, 'printconf'])
if r != 0: if r != 0:
OCAMLFIND='' OCAMLFIND=''
@ -1743,7 +1742,6 @@ def mk_config():
if is_java_enabled(): if is_java_enabled():
print('JNI Bindings: %s' % JNI_HOME) print('JNI Bindings: %s' % JNI_HOME)
print('Java Compiler: %s' % JAVAC) print('Java Compiler: %s' % JAVAC)
print('ML API: %s' % is_ml_enabled())
if is_ml_enabled(): if is_ml_enabled():
print('OCaml Compiler: %s' % OCAMLC) print('OCaml Compiler: %s' % OCAMLC)
print('OCaml Native: %s' % OCAMLOPT) print('OCaml Native: %s' % OCAMLOPT)
@ -1866,11 +1864,10 @@ def mk_config():
if is_java_enabled(): if is_java_enabled():
print('JNI Bindings: %s' % JNI_HOME) print('JNI Bindings: %s' % JNI_HOME)
print('Java Compiler: %s' % JAVAC) print('Java Compiler: %s' % JAVAC)
print('ML API: %s' % is_ml_enabled())
if is_ml_enabled(): if is_ml_enabled():
print('Ocaml Compiler: %s' % OCAMLC) print('OCaml Compiler: %s' % OCAMLC)
print('Ocaml Native: %s' % OCAMLOPT) print('OCaml Native: %s' % OCAMLOPT)
print('Ocaml Library: %s' % OCAML_LIB) print('OCaml Library: %s' % OCAML_LIB)
def mk_install(out): def mk_install(out):
out.write('install: ') out.write('install: ')
@ -2437,9 +2434,6 @@ def mk_bindings(api_files):
if is_java_enabled(): if is_java_enabled():
check_java() check_java()
mk_z3consts_java(api_files) mk_z3consts_java(api_files)
if is_ml_enabled():
check_ml()
mk_z3consts_ml(api_files)
_execfile(os.path.join('scripts', 'update_api.py'), g) # HACK _execfile(os.path.join('scripts', 'update_api.py'), g) # HACK
cp_z3py_to_build() cp_z3py_to_build()
if is_ml_enabled(): if is_ml_enabled():
@ -2808,7 +2802,6 @@ def mk_z3consts_ml(api_files):
decls[words[1]] = idx decls[words[1]] = idx
idx = idx + 1 idx = idx + 1
linenum = linenum + 1 linenum = linenum + 1
efile.write('end\n')
if VERBOSE: if VERBOSE:
print ('Generated "%s/z3enums.ml"' % ('%s' % gendir)) print ('Generated "%s/z3enums.ml"' % ('%s' % gendir))
efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w') efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w')