LlvmReduce

How to report bugs?

If Clam crashes then simply open an issue with the corresponding bitcode file and the exact clam.py command (included all options) needed to reproduce the crash. Even better, you can provide the yaml file so that clam-yaml.py can reproduce the error.

If Clam does not crash but instead it produces a wrong invariant or proves incorrectly an assertion then you can also open an issue as explained before. However, if the bitcode file is large then please try to use llvm-reduce to minimize it.

How to use llvm-reduce with Clam

Suppose that clam.py reports 2 proven assertions and 1 warning but you believe that it should report 2 warnings instead.

You can write a script test-bug.sh like this:

#!/bin/bash

file=$1
./scripts/output_check.py --file $file --safe 2 --warn 1 -- clam.py --crab-check=assert --crab-dom=int --crab-track=mem 
exit $?

This script takes one argument which is the LLVM .bc or .ll file. It returns 0 if and only if the clam command clam.py --crab-check=assert --crab-dom=int --crab-track=mem $file proves 2 assertions and reports 1 warning.

Then, run the command:

llvm-reduce --test=test-bug.sh test.ll 

This will produce a file reduced.ll which is a minimized version (fewer functions, basic blocks, instructions, etc) of test.ll such that clam.py --crab-check=assert --crab-dom=int --crab-track=mem reduced.ll still proves 2 assertions and reports 1 warning.

If you are successful at generating a smaller bitcode file, then add the original and the minimized bitcode when you open the issue.