Error location does not exist

[Marcelo Sousa]

Hello all,

I ran the newest available version of llbmc on a test case and in the logfile I got:

Error location:

===============

Error occurs in basic block "bb10" of function "eval"

The issue is that looking for bb10 inside eval in the bytecode there does not exist. I know that you are performing optimizations and therefore changing the bc file. Can I dump the intermediate version of the bc or I am looking at this in the wrong way?

Kind regards,

Marcelo

[Stephan Falke]

Hi Marcelo,

The released version does not offer an option to dump the bitcode after
the internally applied transformations.

Did you compile your testcase with debug information (using "-g")? If
you do this, then LLBMC will report the line/column in the source code
where the error occurs.

Alternatively, you could run LLBMC with the "--counterexample" option.
This will produce a trace on the LLVM level (after application of the
internal transformations).

Cheers,
Stephan

[Marcelo Sousa]

Hi Stephan,

Compiling the testcase with the debug information does help thanks. Since the counterexample is still at the IR level it's not very useful for long models.

With respect to my testcase I'm still not sure why do I get the error. In attach I send you the .c file and the log file. I'm only interested in verifying my assertions:

llbmc -only-custom-assertions -ignore-missing-function-bodies bist_cell.bc > bist_cell.log

The error synopsis states: Loop iteration bound is not sufficient. The program analysis is thus not complete. 

I have 2 questions regarding this:

1. How do you compute this, i.e. are you performing static analysis of the loop condition and comparing it with the input parameter?  

2. Why do you consider this an error? To me, this seems a natural consequence of performing BMC. In the case of this example since you have a while(1), you won't achieve completeness with 'pure' BMC. 

-- 
Kind Regards,
Marcelo Sousa

[Stephan Falke]

Hi Marcelo,

> Compiling the testcase with the debug information does help thanks.
> Since the counterexample is still at the IR level it's not very useful
> for long models.
>
> With respect to my testcase I'm still not sure why do I get the error.
> In attach I send you the .c file and the log file. I'm only interested
> in verifying my assertions:
>
> llbmc -only-custom-assertions -ignore-missing-function-bodies
> bist_cell.bc > bist_cell.log

I noticed that your C file does not include assert.h. Version 2012.2a
of LLBMC will then not be able to recognize the call to assert as such
and will not check whether it is true. I would suggest you include
assert.h. Alternatively, add a declaration of the form

void __llbmc_assert(int);

to the file and replace the call to assert by a call to __llbmc_assert.

> The error synopsis states: Loop iteration bound is not sufficient. The
> program analysis is thus not complete.
>
> I have 2 questions regarding this:
> 1. How do you compute this, i.e. are you performing static analysis of
> the loop condition and comparing it with the input parameter?

This is determined by the SMT solver since LLBMC adds an assertion that
checks whether the loop bound is sufficient. The SMT solver then found
out that this assertion fails.

> 2. Why do you consider this an error? To me, this seems a natural
> consequence of performing BMC. In the case of this example since you
> have a while(1), you won't achieve completeness with 'pure' BMC.

We consider it an error since we don't want the give the user the false
impression that LLBMC has verified that the program is error-free. You
can disable the checks for loop bounds by passing the option
"-no-max-loop-iterations-checks" to LLBMC. In your example, providing
this option will cause LLBMC to check the assertion only for those runs
of the program where the loop iteration bound that you provide is
sufficient.

Best regards,
Stephan

[Marcelo Sousa]

Hello Stephan,

I changed assert to __llbmc_assert but I still get the same log error. Do you have any other suggestions?

Kind regards,

Marcelo

[mriccobene]

Hello Marcelo,

if this can help you, I replaced nondet_int() with __llbmc_nondef_int(), I included "llbmc.h" and I tried this:

clang -c -g -emit-llvm bist_cell.c -o bist_cell.bc

llbmc -no-max-loop-iterations-checks -only-custom-assertions  bist_cell.bc

I did not get any error:

This is the Low-Level Bounded Model Checker LLBMC (version 2012.2a).

Running LLBMC with automatically determined function call depth and at most 0 iterations for loops with non-derivable trip count.

1 assertion before simplification (1 custom).

Performing formula transformations and simplifications... done.  [0.012 sec]

0 assertions remain after simplification.

Running SMT solver (STP with MiniSat)... done.  [0.000 sec]

Result:

=======

No error detected.

(i am using clang version 3.1)

Michelangelo