S3L-official / CT_Prover

MIT License
2 stars 0 forks source link

Errors during execution of ./bootstrap.sh #1

Open pieroo98 opened 1 month ago

pieroo98 commented 1 month ago

Hi, I was installing the tool, but I had several problems after executing the command . /bootstrap.sh, below the photos of the errors. It does not find the path "external". Below is the list of steps performed to install the tool on Ubuntu 22.04:

Here after about 4/5 hours of automatic setting gave me these 4 errors on the path not found. How can I fix? CT_Prover

pieroo98 commented 1 month ago

This problem is due to the missing folder "external". This folder contains four repo that could be installed all together with the commands : git submodule init git submodule update but these commands didn't work! so I have to install manually inside the path /CT_Prover/phasar in this way :

git clone https://github.com/nlohmann/json.git external/json
git clone https://github.com/google/googletest.git external/googletest
git clone https://github.com/pdschubert/Wali-OpenNWA.git external/WALi-OpenNWA
git clone https://github.com/pboettch/json-schema-validator.git external/json-schema-validator

After that, I execute inside each repo, the commands written in the README.md file, that are these :

mkdir build
cd build
sudo cmake ..
sudo make 
sudo make install

With this commands the file ./bootstrap.sh was executed without that error, but another error arise : err2 The path /home/luwei/newwids/SVF/Release-build/svf-llvm/libsvfLLVM.a is incorrect, I haven't a path named luwei inside the home directory. The program get this path from the file ~CT_Prover/phasar/lib/PhasarLLVM/DataFlowSolver/IfdsIde/CMakeLists.txt, but this path is wrong and the file libsvfLLVM.a doesn't exist. Probably there are some commands that must be executed before and the file CMakeLists.txt is left with the developer configuration. (screen of CMakeList.txt below )

config

In fact the name 'luwei' is the name of the author.

To resolve This other error is possible to install SVF from git :

git clone https://github.com/SVF-tools/SVF.git
cd SVF
sudo ./build.sh
mkdir Release-build
cd Release-build
cmake -G Ninja .. -DCMAKE_BUILD_TYPE=Release
sudo ninja

and then change in the file ~CT_Prover/phasar/lib/PhasarLLVM/DataFlowSolver/IfdsIde/CMakeLists.txt the lines that refers to libsvfLLVM.a, libz3.a and libz3.so with the correct path (get it from the new SVF project) . This change must be done in other files, like : ~CT_Prover/Extern_PTA/SVF-example/CMakeLists.txt ~CT_Prover/Extern_PTA/SVF-example/src/CMakeFiles/svf-ex.dir/build.make ~CT_Prover/Extern_PTA/SVF-example/src/CMakeFiles/svf-ex.dir/link.txt At this point execute again ./bootstrap.sh but other errors occurs.

pieroo98 commented 1 month ago

I have also tried to create a new user inside my home directory, with the same name of the owner : "luwei", and I have installed SVF and CT_Prover inside the path "newifds" in order to set the same path, but neither in this way I was able to execute the command "./bootstrap" without errors.