Skip to content
Snippets Groups Projects
user avatar
Etienne Kneuss authored
options differently, not yet finished
38a639c9
History
This is Leon 0.2.0

To build it, you will need, for example, the following:
  * Java Runtime Environment, from Oracle, e.g. Version 7 Update 5 
    (to run xsbt and scala)
  * Scala, from Typesafe, e.g. version 2.9.1
  * xsbt, e.g. version 0.11.3: download sbt-launch.jar, run it with java -jar
    (to built Leon)
  * a recent GLIBC3 or later, works with e.g. apt-get
    (for Z3)
  * GNU Multiprecision library, e.g. gmp3, works with e.g. apt-get
    (for Z3)

To build, type this:

xsbt clean   
xsbt package # takes a while
xsbt script

Then you can try e.g.

./run-demo demo/RedBlackTree.scala

and get something like this:

[ Info  ] . ┌─────────┐
          ╔═╡ Summary ╞═══════════════════════════════════════════════════════════════════════╗
          ║ └─────────┘                                                                       ║
          ║ add                       postcond.           valid               Z3-f+t    0.314 ║
          ║ add                       precond.    (82,14) valid               Z3-f+t    0.020 ║
          ║ add                       precond.    (82,18) valid               Z3-f+t    0.005 ║
          ║ balance                   postcond.           valid               Z3-f+t    0.409 ║
          ║ balance                   match.      (91,19) valid               Z3-f+t    0.034 ║
          ║ blackHeight               match.      (51,39) valid               Z3-f+t    0.004 ║
          ║ buggyAdd                  postcond.           invalid             Z3-f+t    4.084 ║
          ║ buggyAdd                  precond.     (87,8) invalid             Z3-f+t    0.111 ║
          ║ buggyBalance              postcond.           invalid             Z3-f+t    0.055 ║
          ║ buggyBalance              match.     (105,19) invalid             Z3-f+t    0.007 ║
          ║ ins                       postcond.           valid               Z3-f+t    6.577 ║
          ║ ins                       precond.    (63,40) valid               Z3-f+t    0.021 ║
          ║ ins                       precond.    (65,43) valid               Z3-f+t    0.005 ║
          ║ makeBlack                 postcond.           valid               Z3-f+t    0.007 ║
          ║ redNodesHaveBlackChildren match.      (35,56) valid               Z3-f+t    0.003 ║
          ║ size                      postcond.           valid               Z3-f+t    0.012 ║
          ╚═══════════════════════════════════════════════════════════════════════════════════╝

Additional information:
=======================
Sample output of 
  ldd lib-bin/lib3.so
is:
	linux-gate.so.1 =>  (0x00b13000)
	libgmp.so.3 => /usr/lib/libgmp.so.3 (0x00110000)
	libstdc++.so.6 => /usr/lib/i386-linux-gnu/libstdc++.so.6 (0x0016f000)
	libm.so.6 => /lib/i386-linux-gnu/libm.so.6 (0x0025a000)
	libgcc_s.so.1 => /lib/i386-linux-gnu/libgcc_s.so.1 (0x00709000)
	libc.so.6 => /lib/i386-linux-gnu/libc.so.6 (0x004d9000)
	/lib/ld-linux.so.2 (0x002ab000)