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
Previous revision
Next revision Both sides next revision
scalaz3 [2011/08/03 14:44]
vkuncak
scalaz3 [2011/10/20 16:41]
philippe.suter
Line 26: Line 26:
  
 We're not actively developing the Java library. However, the JNI bindings are common for the Scala and Java API, so the effort required to write the Java library is minimal (eg. you do not need to know anything about the JNI). Let us know if you are interested in doing that. We're not actively developing the Java library. However, the JNI bindings are common for the Scala and Java API, so the effort required to write the Java library is minimal (eg. you do not need to know anything about the JNI). Let us know if you are interested in doing that.
 +
  
  
Line 35: Line 36:
 ===== Installation ===== ===== Installation =====
  
-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 can get the sources from [[http://​github.com/​psuter/​ScalaZ3|GitHub]]. ​Precompiled ​versions ​are also available ​from there.
  
 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.19 (we have not seen changes in the API since version ​2.11, though).+Currently, the bindings are compiled against Z3 3.2.
  
 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 55: Line 56:
 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 a 64bit machine). 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 a 64bit machine).
  
-==== Windows Usage Notes ==== 
  
-Aside from the ''​z3.dll''​ shared library, you will need two libraries that come as part of the  +
-[[http://​www.microsoft.com/​downloads/​en/​details.aspx?​displaylang=en&​FamilyID=a7b7a05e-6de6-4d3a-a423-37bf0912db84|Microsoft Visual C++ 2010 Redistributable Package]].+
  
 ===== Authors ===== ===== Authors =====