LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision Both sides next revision
jniz3 [2011/07/29 16:31]
philippe.suter
jniz3 [2011/07/29 16:36]
philippe.suter
Line 27: Line 27:
  
  
-===== Download ​=====+===== Installation ​=====
  
-You can get the latest ''​z3.jar''​ (including the Scala class files, the Java class files and the C bindings) ​from [[http://lara.epfl.ch/~psuter/jniz3|here]]. Note that we don't currently distribute ​the sources.+You can get the sources ​from [[http://github.com/psuter/ScalaZ3|GitHub]]. We also plan to make precompiled versions available for download in the future.
  
 You'll need the shared library ''​libz3.so''​ or ''​z3.dll''​. See Microsoft Research'​s website [[http://​research.microsoft.com/​en-us/​um/​redmond/​projects/​z3/​download.html]]. You'll need the shared library ''​libz3.so''​ or ''​z3.dll''​. See Microsoft Research'​s website [[http://​research.microsoft.com/​en-us/​um/​redmond/​projects/​z3/​download.html]].
  
-Currently, the bindings are compiled against Z3 2.15 (we have not seen changes in the API since version 2.11, though). Note that the Linux version reports 2.16 as the version number.+Currently, the bindings are compiled against Z3 2.19 (we have not seen changes in the API since version 2.11, though).
  
 We try hard to make all functions safe by wrapping Z3 pointers into proper classes, so that all calls can by typechecked by Scala/Java. However, there are always ways to break things. Be aware of the following (from: G. Tan et al., //Safe Java Native Interface//,​ IEEE Symp. on Secure Software Engineering,​ 2006): We try hard to make all functions safe by wrapping Z3 pointers into proper classes, so that all calls can by typechecked by Scala/Java. However, there are always ways to break things. Be aware of the following (from: G. Tan et al., //Safe Java Native Interface//,​ IEEE Symp. on Secure Software Engineering,​ 2006):
Line 43: Line 43:
 ===== Temporary Files ===== ===== Temporary Files =====
  
-When you use the jar file, it will unpack the required native bindings (''​libjniz3.so''​ for *nix variants, and ''​jniz3.dll''​ for Windows) ​to a temporary directory. This is required for the JVM to be able to load the library, as it can only load libraries from the OS file system. A directory ''​JNIZ3_????-??-??'',​ where the question marks are replaced by the date, is created in the default temporary directory (''/​tmp/'',​ ''​C:​\users\UserName\AppData\Local\Temp''​ for Windows 7, etc.). ​**Warning:​** currently, if you use two different versions of ''​z3.jar''​ the same day, you run the risk of triggering ''​UnsatisfiableLinkError''​ exceptions. We will probably fix this in future releases by attaching the version number to the temporary directory. +When you use the jar file, it will unpack the required native bindings (''​libscalaz3.so''​ for *nix variants, and ''​scalaz3.dll''​ for Windows) ​in a temporary directory. This is required for the JVM to be able to load the library, as it can only load libraries from the OS file system. A directory ''​SCALAZ3_??????'',​ where the question marks are replaced by a hash of the library version, is created in the default temporary directory (''/​tmp/'',​ ''​C:​\users\UserName\AppData\Local\Temp''​ for Windows 7, etc.).
- +
- +
  
 ===== Applicability ===== ===== Applicability =====
  
-The current version works on architectures running a variant of Linux or Windows. ​We have not personally tested ​the library on 64bit architectures yet and would appreciate any feedback on that subject. //In theory//, it should work. +The current version works on architectures running a variant of Linux or Windows. ​It works regardless of the underlying architecture (32 or 64bit), *as long as* the JVM uses the same architecture:​ you cannot use the library ​with a 32bit JVM running ​on 64bit machine).
  
 ==== Windows Usage Notes ==== ==== Windows Usage Notes ====
Line 63: Line 59:
  
  
-===== Change Log ===== 
- 
-(The following is a non-exhaustive list of changes.) 
- 
-  1.1   ​2010-12-03 ​  ​Included DLL for Windows, Z3AST instances can be built easily from others using overloaded operators, support for the SMT LIB parser interface. 
-  1.0   ​2010-09-16 ​  ​Initial release.