Missing Warning

[IreneStergioti]

Hello,

I was running clam using crab version 77294ec9d8932b9a8bcebc26c2d8827ddac58798 and a pair of almost identical files; initial.ll and transformed.ll.

To be more precise, the initial.ll file had the following 2 assumptions:

; in function thr2 

_7:                                               ; preds = %_4
  %crab_ = sub i32 0, %_5
  %crab_56 = icmp sle i32 %crab_, -1
  call void @verifier.assume(i1 %crab_56)
  [...]

_store7:                                          ; preds = %_4
  %crab_71 = add i32 0, %_5
  %crab_72 = icmp sle i32 %crab_71, 0
  call void @verifier.assume(i1 %crab_72)
  [...]

These 2 assumptions were replaced in transformed.ll by call void @verifier.assume(i1 true)

I executed both of these files with the command: clam.py --no-preprocess --crab-check=assert --crab-dom=zones --crab-disable-warnings --crab-track=sing-mem --crab-lower-unsigned-icmp=true --crab-backward --crab-widening-delay=8 --crab-narrowing-iterations=4 --crab-widening-jump-set=10 file.ll

The results for initial.ll were:

************** ANALYSIS RESULTS ****************
3  Number of total safe checks
0  Number of total error checks
3  Number of total warning checks
************** ANALYSIS RESULTS END*************

And for transformed.ll :

 ************** ANALYSIS RESULTS ****************
4  Number of total safe checks
0  Number of total error checks
2  Number of total warning checks
************** ANALYSIS RESULTS END*************

The fact that transformed.ll resulted in fewer warnings than initial.ll, was not really expected, given that it, basically, had less assumptions in it. files.zip

[caballa]

Fixed in commit 25e920f16fcde29957c4407d23e4df596ad2b7fd