Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama/Clang Issues

  • Subject: [Frama-c-discuss] Frama/Clang Issues
  • From: richardlford at gmail.com (Richard Ford)
  • Date: Fri, 8 May 2020 17:38:46 -0500
I've been testing out Frama-C (20.0/Calcium) and Frama/Clang (0.0.8)
recently and have encountered some issues. I realize Frama/Clang is still
in an early stage of development but thought I would report these anyway.

1. When the Ocaml part of Frama/Clang is converting the intermediate_format
to the cabs format, it forces the *this* pointer for constructor and
destructor functions to be pointer to *const* struct. But these, at least
the constructor, do change the object being constructed. If the "-print
-ocode file.c" option is used to produce the C code that has been lowered,
the presence of those "const"s gives compile-time errors. I currently have
patched the convert.ml file to avoid adding the const. Is there a reason
why these were added?

2. Trying to process any program which includes <iostream> fails because
the error:

.../share/frama-c/frama-clang/libc++/ostream:35:40:
      error: implicit instantiation of undefined template
'std::basic_ios<char, std::char_traits<char> >'

This is because there is no definition of basic_ios supplied.

3. Trying to use <stdio.h> leads to these warnings but at least processing
does not stop:
<install-root>/share/frama-c/libc/stdio.h:309:33: unexpected token 'keyword
-> reads' in logic function/predicate definition
<install-root>/share/frama-c/libc/stdio.h:314:44: unknown identifier
'gets_length'
<install-root>/share/frama-c/libc/stdio.h:532:42: keyword 'keyword -> type'
encountered when parsing term or predicate

4. Trying a somewhat more complex example gave errors like this:

<install-root>/share/frama-c/libc/signal.h:223:28: Expecting ';' after
requires clause
<install-root>/share/frama-c/libc/wchar.h:55:5: No suitable candidate found
for function valid_read_or_empty.
<install-root>/share/frama-c/libc/wchar.h:69:74: No suitable candidate
found for function valid_read_or_empty.
<install-root>/share/frama-c/libc/wchar.h:80:73: No suitable candidate
found for function valid_or_empty.
<install-root>/share/frama-c/libc/math.h:134:40: unknown identifier
'\is_infinite'
<install-root>/share/frama-c/libc/math.h:148:40: unknown identifier
'\is_infinite'
<install-root>/share/frama-c/libc/math.h:158:38: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:176:40: unknown identifier
'\is_infinite'
<install-root>/share/frama-c/libc/math.h:190:40: unknown identifier
'\is_infinite'
<install-root>/share/frama-c/libc/math.h:200:38: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:225:39: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:233:45: calls to C++
functions/methods like 'atan2' are not allowed in ACSL++
<install-root>/share/frama-c/libc/math.h:240:52: calls to C++
functions/methods like 'atan2f' are not allowed in ACSL++
<install-root>/share/frama-c/libc/math.h:262:39: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:283:39: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:301:48: unknown identifier
'\is_plus_infinity'
<install-root>/share/frama-c/libc/math.h:319:48: unknown identifier
'\is_plus_infinity'
<install-root>/share/frama-c/libc/math.h:333:38: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:420:39: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:441:39: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:466:39: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:509:39: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:522:46: calls to C++
functions/methods like 'pow' are not allowed in ACSL++
<install-root>/share/frama-c/libc/math.h:529:47: calls to C++
functions/methods like 'powf' are not allowed in ACSL++
<install-root>/share/frama-c/libc/math.h:553:39: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:590:39: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:608:39: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:642:39: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:668:39: No suitable candidate
found for function \is_finite.
<install-root>/share/frama-c/libc/math.h:675:50: calls to C++
functions/methods like 'fmod' are not allowed in ACSL++
<install-root>/share/frama-c/libc/math.h:682:51: calls to C++
functions/methods like 'fmodf' are not allowed in ACSL++
<install-root>/share/frama-c/libc/math.h:719:42: No suitable candidate
found for function \is_NaN.
<install-root>/share/frama-c/libc/math.h:759:56: unknown identifier
'\plus_infinity'
<install-root>/share/frama-c/libc/math.h:765:48: unknown identifier
'\is_plus_infinity'

5. Deciding to not use the include files from frama-c, I instead hit some
errors like this:

Unknown kind of comment at
/usr/lib/gcc/x86_64-linux-gnu/7.5.0/../../../../include/c++/7.5.0/bits/stl_iterator_base_types.h:87:87:38

The specified line has this content:

  //@{

In searching through the /usr/include directory I find many such lines. So
perhaps something should be done
to specifically ignore these as they seem related to some coding convention.

6. Difficulty debugging dynamically-loaded OCaml code.
This is more a comment for an Ocaml forum, but I find ocamldebug to be
lacking in a variety of ways. A standard way I have of learning about a
program is to step through parts of it in the symbolic debugger. So
starting to study Frama-C and Frama/Clang I naturally wanted to do the same
thing. Things went well as long as I was in the main part of Frama-C,
though I found its use of modules somewhat difficult. And I'm used to
having a debugger be able to call functions in the user program that will
print out data structure that are too complicated for the debugger itself
to figure out. But when I tried to step into the dynamically loaded
Frama/Clang plug-in (the Ocaml part), it did not know about it. So it seems
not to know about symbols in dynamically loaded modules. I did step into
ocamlrun (with gdb) to see how it works, and how dynamic loading works. It
does load in the events (i.e. places to step to).

In any case, my solution was to figure out how to build the Frama/Clang
plugin so it is statically part of Frama-C. Then I was able to step into
it. The one hitch was that I had to rename its Meta file or else Frama-C
would try to register it twice.

That's all for now. I'm impressed with the progress so far. I was
interested to learn that Frama-C's two IRs, Cabs and Cil both have throw
and catch, and that there is a phase to eliminate exception handling.

As far as include files are concerned, it would be helpful if the
developers would try test programs that just include each header file
individually using Frama/Clang to make sure they are at least consistent
and  complete enough to compile.

Thanks for your effort.

Richard L Ford
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200508/5ca257d3/attachment.html>