Unknown bitstream version!

[ye_beloved]

Hi,

    when I run the example $llbmc double-free.bc, I got

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.

Could not parse bitcode file.

Unknown bitstream version!

Is it because my clang version is 3.2?

Besides, could you tell me what language do you use to implement llbmc? If the source code or more details about implementation can be offered, it will do much more help to me.

Thank you so much.  

[Stephan Falke]

Hi Anonymous,

> when I run the example $llbmc double-free.bc, I got
>
> 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.
>
> Could not parse bitcode file.
> Unknown bitstream version!
>
> Is it because my clang version is 3.2?

Yes. LLVM's bitcode format is generally not compatible between
different versions. LLBMC 2012.2a only supports the bitcode format of
version 3.1, so you need to use clang version 3.1 to produce your
bitcode files.

> Besides, could you tell me what language do you use to implement llbmc? If
> the source code or more details about implementation can be offered, it
> will do much more help to me.

LLBMC itself is implemented in C++. Unfortunately, the source code is
currently not available.

Cheers,
Stephan