kaled-alshmrany / fusebmc Goto Github PK

In TestComp we will need to generate a release to be used by external environments so we could use something like make release, it should:

• Be static
• Contain the wrapper (named as esbmc-wrapper.py), esbmc, and the instrumentation tool.

If it generated something like fusebmc.tar.gz it would be great.

The download link to ESBMC in the README is no longer available as that project changed its build infrastructure. Could you instead please point to the esbmc-linux.zip, e.g. https://github.com/esbmc/esbmc/releases/download/v7.5/esbmc-linux.zip for v7.5 (in case you want to update it from v7.4).

I tried to compile but the following issue occurred.

make clean release
rm -f obj/*.o
rm -f FuSeBMC_inustrment
/home/kaled/Downloads/clang_base/bin/clang++ -Wall -Wextra -W -std=c++11 -I./include -I/home/kaled/Downloads/clang_base/include -I/mnt/sda2/llvm-6.0.0/include  -fno-rtti  -Wno-unsequenced -Wno-unused-parameter -o3 -os  -c src/GoalCounter.cpp -o obj/GoalCounter.o
make: /home/kaled/Downloads/clang_base/bin/clang++: No such file or directory
make: *** [Makefile:26: obj/GoalCounter.o] Error 127

Checking the Makefile the CLANG_BASE is hardcoded:

 CLANG_BASE = /home/kaled/Downloads/clang_base  

Currently, the repository contains files that shouldn't be tracked e.g. build files and property files this makes harder to track which files are important. There should be a .gitignore for those files.

Running ./my_instrument --input test.c --output ./my_instrument_outpt/instrumrnted.c --goal-output-file ./my_instrument_outpt/goals.txt --add-else --add-labels throws an error if the output directory does not exist.

While compiling instrumented code, is there a way to pass compiler flags to it without hardcoding it in the fusebmc.py.
Also I'm getting lstFuSeBMC_GoalTracerGoals=[] and lstFuSeBMC_FuzzerGoals_Run2=[] but I think that's because fusebmc cant compile the instrumented code as it has a set of flags that are not being set.

The Wrapper is returning FAIL_COVER_ERROR_CALL or FAIL_COVER_BRANCHES. It should be DONE

Relevant files:

• Wrapper: https://github.com/kaled-alshmrany/FuSeBMC/blob/master/my_wrapper/my_esbmc_wrapper_final_001.py#L663-L667

Explanation:

Benchexec integrates with each tool with a custom module, ESBMC's module is here, last years competition it was decided that when the tool finished it should output a DONE result in TestComp.

There are some hardcoded paths in the wrapper. The wrapper should rely on PATH to get the binaries.

Example: https://github.com/kaled-alshmrany/FuSeBMC/blob/master/my_wrapper/my_esbmc_wrapper_final_001.py#L33

Just remove all of them.