Analyzing a simple C++ program with Frama-C

Question

I started learning C++ from a great tutorial available at https://learnxinyminutes.com/docs/c++/ and would like to analyze in Frama-C a simplest example that shows references:

using namespace std;
#include <iostream>
#include <string>

int main() {
    string foo = "I am foo";
    string bar = "I am bar";

    string& fooRef = foo; // This creates a reference to foo.
    fooRef += ". Hi!"; // Modifies foo through the reference
    cout << fooRef; // Prints "I am foo. Hi!"

    // Doesn't reassign "fooRef". This is the same as "foo = bar", and
    //   foo == "I am bar"
    // after this line.
    cout << &fooRef << endl; //Prints the address of foo
    fooRef = bar;
    cout << &fooRef << endl; //Still prints the address of foo
    cout << fooRef;  // Prints "I am bar"

    //The address of fooRef remains the same, i.e. it is still referring to foo.
    return 0;
}

I compiled and installed Frama-C C++ plug-in called "Frama-Clang". Now when I run frama-c I get warnings and errors in the output:

$ frama-c refs.cc 
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing refs.cc (external front-end)
refs.cc:13:17: warning: using directive refers to implicitly-defined namespace 'std'
using namespace std;
                ^
In file included from refs.cc:14:
In file included from /usr/share/frama-c/frama-clang/libc++/iostream:29:
/usr/share/frama-c/frama-clang/libc++/ostream:31:40: error: implicit instantiation of undefined template 'std::basic_ios<char, std::char_traits<char> >'
  class basic_ostream : virtual public basic_ios<charT,traits> {
                                       ^
refs.cc:23:7: note: in instantiation of template class 'std::basic_ostream<char, std::char_traits<char> >' requested here
        cout << fooRef; // Prints "I am foo. Hi!"
             ^
/usr/share/frama-c/frama-clang/libc++/iosfwd:37:68: note: template is declared here
  template <class charT, class traits = char_traits<charT> > class basic_ios;
                                                                   ^
code generation aborted due to one compilation error
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: stopping on file "refs.cc" that has errors.
[kernel] Frama-C aborted: invalid user input.

What is wrong?

(Frama-C is installed from a debian-testing repository in version 20170501+phosphorus+dfsg-2)

The code itself [seems reasonably ok](http://coliru.stacked-crooked.com/a/4bdeae3aa60f76a2). The problem seems to be Frama having failed to set up clang to understand system headers correctly. — nwp, Oct 12 '17 at 14:48
Move `using namespace std;` after the `#include`s. Or better: [don't use it](https://stackoverflow.com/questions/1452721/why-is-using-namespace-std-considered-bad-practice). — O'Neil, Oct 12 '17 at 15:00
Don't you need to preprocess your source files before sending them to frama? — user7860670, Oct 12 '17 at 15:02
@VTT the preprocessing happens automatically; in the GUI I can also choose ".cc" files now — tomasz, Oct 12 '17 at 20:04
@O'Neil Thank you for the tip before I got used to that bad practice! — tomasz, Oct 12 '17 at 20:06
How is that even possible? It will need to figure out build settings somehow. Could you post some relevant link for this matter? — user7860670, Oct 12 '17 at 20:09
@VTT I found this sentence at https://frama-c.com/frama-clang.html: "When this plug-in is in use, Frama-C will consider all files ending in .cpp, .c++, .C, .cxx, .cc and .ii (considered as already pre-processed) as C++ files and give them to Frama-Clang" — tomasz, Oct 13 '17 at 08:45

score 4 · Answer 1 · answered Oct 12 '17 at 18:07

First of all, I'd like to point out the caveat on the Frama-Clang page:

Frama-Clang is currently in an early stage of development. It is known to be incomplete and comes without any bug-freeness guarantee.

Thus, if you're not already familiar with C++, I'd kindly suggest that starting right away with Frama-Clang might be a pretty big effort.

That said, the issue is, as mentioned in the comments, that STL support in Frama-Clang is minimal (in particular, the innocent-looking iostream is not exactly the easiest piece of code to handle when it comes to templates).

You might have better luck by using frama-c -cxx-nostdinc refs.cc, which will use your system's standard library instead of the one shipped with Frama-Clang: this will at least let clang type-check your code. There is however absolutely no guarantee that Frama-Clang itself will be able to understand all the constructions provided by this library.

thank you. I replaced `using namespace std` with separate `using std::cout`/`string`/`endl` and used `-cxx-nostdinc`; the error now is clearer: `[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)` `[kernel] Parsing refs.cc (external front-end)` `: Unsupported Type (uninstantiated template specialization):allocator` `Aborting` `[kernel] user error: Failed to parse C++ file. See Clang messages for more information` — tomasz, Oct 13 '17 at 08:42

Analyzing a simple C++ program with Frama-C

1 Answers1

Linked