Benchmark LLVM frontend
To find out how well our LLVM frontend works, at the moment, we should run benchmarks with and without -clang
on the sv-benchmarks.
Identified bugs and differences should be documented (bugs as issues, differences here, for now).
First, we should check crashes in the frontend with -generateCFA
.
Then, to check analysis, I would start with property unreach-call
, because most small programs are easy to manually analyze for that property. This makes evaluation easier.
In addition, properties no-overflow
and termination
would be interesting.
For memsafety properties, I would assume that CPAchecker can't solve them anymore after translation to LLVM, because memory-specific functions may get lost.
As a starting point, one could use the svcomp21--* benchmark definitions, e.g., svcomp21--reachsafety.xml .
Instead of -svcomp21
, I would use configuration valueAnalysis-NoCegar
because of its simplicity, and later predicateAnalysis
to ensure compatibility of the LLVM frontend with different analyses.
Summary: Check for bugs, missing features and inherent dis(advantages) compared to native analysis on the following tasks:
-
all tasks with -generateCFA
-
unreach-call
with value analysis -
no-overflow
with value analysis -
termination
with value analysis -
Check whether memsafety
-properties don't work with LLVM frontend -
Repeat all of the above with predicate analysis