Any feedbacks, advises and questions are welcomed. Feel free to ask any question by sending an email to lixie19[AT]ios[DOT]ac[DOT]cn or by creating an issue.
SESL is a tool for memory safety checking. It is an symbolic execution extension of existing state-of-the-art tool SMACK on separation logic.
We build our tool based on
- SMACK: We brought the frontend of SMACK into use, which provides a magnificant translation from source code to Boogie IVL based on LLVM passes.
System requirement:
- Linux (Ubuntu 20.04 LTS)
- Python 3.6 and above
- CMake and Ninja build
Required libraries:
-
Z3
Installation of Z3 can be found HERE.
Please notice since the tool is built using CMake, install Z3 by CMake is a must.
-
LLVM, Clang and OpenSSL
sudo apt-get install llvm clang sudo apt-get install openssl sudo apt-get install libssl-dev
SESL reused framework of SMACK, therefore the installation mainly follows the instructions in . Specifically, in the root path execute the build script provided by SMACK:
cd bin
./build.sh
If the above build file failed, one can manually build install Z3 and build the tool by:
mkdir build
cd build
cmake -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_BUILD_TYPE=Debug .. -G Ninja
# this command will install sesl for your system
sudo ninja install
If you install sesl for global, you can check the installation by running sesl --version
.
sesl --version
version 1.0.1
After installation, you can run our tool globally. It is recommended to use the following command to analyze one single file:
sesl -bw 64 -t --sh-mem-leak --add-line-info <input_file>
where -t --sh-mem-leak --add-line-info
are musts, and -bw 64
indicates the architecture considered for the checking is 64bit machine, one can also use -bw 32
to identify 32bit architecture.
Test cases are listed in folder testcases
. Three scripts sv_debug_c.sh
, sv_debug_i.sh
and test_debug.sh
in bin
are used to test cases. For example,
cd bin
./test_debug.sh exec
This will compile the tool and then run an example in folder testcases/printtest/exec.c
For convenience, the link of all the testcases of Memory-Safety of SV-COMP can be found in testcases/svcomp/overall
except for Juliet_Test
.