We offer a binares file, which can be executed in ubuntu 64bit(>= 14.04).
Execute:
./arrayAnalysis_x64 ../testcase/array.cpp --
If it can not be executed in your linux system. you can build it.
Building InvariantSynthesisForArray_C using Z3 and Clang
-
you must build Z3 in your system. please see it in https://github.com/Z3Prover/z3
-
you must build clang(>=3.6.2) in your system. please see it in http://clang.llvm.org/get_started.html.
-
cd src, edit compile.sh, set LLVM_SRC_PATH, LLVM_BUILD_PATH, LLVM_BIN_PATH, z3_src_path and z3_build_path, then run compile.sh