Installing and running LCT
This page explains how to install and use LCT in the computer rooms of the VUB (tested in room E.1.4).
A VM exists with LCT and other tools pre-installed
(http://soft.vub.ac.be/~cderoove/sq/testing-ubuntu-12.10-desktop-i386.zip,
username: ubuntu, password: reverse), but there is unfortunately not enough room
in the computer rooms (neither on the home directory nor in /tmp
) to download
it and unzip it. However, the manual installation is not that hard and probably
takes less time than downloading the entire VM.
1 Installation
Typing the following commands will install LCT on those rooms (no adaptation of path needed):
cd /tmp wget http://www.tcs.hut.fi/Software/lime/LimeTB-2.2.0.tar.gz tar xvf LimeTB-2.2.0.tar.gz export PATH=$PATH:/tmp/LimeTB-2.2.0/bin cd LimeTB-2.2.0/dependencies/solvers wget http://fmv.jku.at/boolector/boolector-1.4-ffc2089-100608.tar.gz wget http://fmv.jku.at/picosat/picosat-936.tar.gz export JAVA_HOME=/usr/lib/jvm/java-7-openjdk-amd64 export JRELIBPATH=$JAVA_HOME/jre/lib make
To test if the installation succeeded, launch limegui
. However, don't use
limegui
to use LCT as there is a bug that prevents you from correctly running
LCT with it.
2 Path adaptation
Once LCT is installed, if you open a new terminal you will have to adapt the
paths again. To avoid that, you can edit the ~/.bashrc
file and add this at
the end:
export JAVA_HOME=/usr/lib/jvm/java-7-openjdk-amd64 export JRELIBPATH=$JAVA_HOME/jre/lib export PATH=$PATH:/tmp/LimeTB-2.2.0/bin
However, you will still need to install LCT at each session as it is stored in a temporary directory.
3 Usage
To use LCT, first launch the server in a terminal:
LCTserver
Then, open another terminal, place yourself in the directory where you have the
.java
file you want to run with LCT, and type the following:
LCTcompile File.java
LCTinstrument File
cd output
LCTrun File all
You can test it on the following program for example.
import fi.hut.ics.lime.tester.LCT; public class Foo { public static void main(String[] args) { int x = LCT.getInteger(); System.out.println(x); } }
4 Importing in Eclipse
To import LCT in Eclipse, launch Eclipse and do the following steps.
- File -> Import -> General -> Existing Projects into Workspace -> Next.
- Choose
/tmp/LimeTB-2.2.0/
as root directory and select onlyLCT
in the projects list, then click Finish. - Import the needed dependencies: Right click on LCT -> Properties -> Java
Build Path -> Add External JARs
- add all the JARs in /tmp/LimeTB-2.2.0/lib/external
- add
/usr/share/java/junit.jar
5 Exporting a JAR
If you want to test modifications done on LCT source code, do the following:
- File -> Export -> Java -> JAR file -> Next.
- Check the LCT box, and set the export destination to
/tmp/LimeTB-2.2.0/lib/lime/LCT-2.2.0.jar/
- Click Finish. Confirm that you want to override the existing file. You might get a warning that the JAR file was exported with warning, but you can just ignore that.
On the next run of LCT, it will use your modified version. If you modified code
in the server, don't forget to relaunch LCTserver
as well.