Dear Chris,
first, thanks for trying to install it !
Frama-C is one of a number of tools we are considering, so it's not a done
deal.
If used, it would only be applied to a small part of the codebase:
typically code that is very critical, but hard to test reliably.
I would expect that this code would be unlikely to change much, if at all.
The contents of the annotations would have to be maintained by those familiar
with
the annotation language(ACSL*) and how it should be used.
They would also be responsible
for ensuring that any loop annotations in .c files would be revised if there
was any significant
code refactoring that altered the number or purpose of those loops.
The annotation in the .h files capture the specification of what the code
should do,
as pre/post-condition pairs - once setup and validated, they shouldn't change
much.
Frama-C has two main components:
` frama-c` : a command line tool that does all the work, and is highly
automatable
`frama-c-gui` : a nice GUI that interacts with `frama-c`, and produces
verification results
that can be re-run from the command line.
The plan is that the GUI might be used to develop/debug/validate the various
annotations,
but that the day-to-day use of Frama-C as part of the qualification toolset
would simply
involve re-running the verifications using the command-line tool, all
automated. It would
only be if this reported some verification failure that any action would need
to be taken.
This would mean that only the command-line tool would need to be installed,
which might
reduce the package count somewhat.
A quick potted history of Frama-C was that it was developed, starting in 2010,
by CEA (http://www-list.cea.fr/en/ <http://www-list.cea.fr/en/>) on top of a
previous tool called CAVEAT they had
that was used internally by Airbus. It was designed specifically to automate
formal
verification of Airbus C code, and then made available to the community at
large.
An issue with it is that it handles C99, but not C11, which may be a
show-stopper for us.
Regards, Andrew
* ACSL = "ANSI C Specification Language"
> On 10 Sep 2019, at 02:36, Chris Johns <chr...@rtems.org> wrote:
>
> On 6/9/19 9:40 pm, Andrew Butterfield wrote:
>> However, if the implementation code contains loops, then we need annotations
>> in
>> the code at those loops. The following, from the Frama-C ACSL Tutorial
>> (https://frama-c.com/acsl_tutorial_index.html) shows the annotations
>> required to
>> verify the correctness of a function that finds the maximum of a sequence of
>> integers.
>
> Am I to assume Frama-C is the analysis tool for this work?
>
> I have taken a look at this tool however it would be nice to get some
> understanding of its history and how you see it fitting in to the RTEMS
> project
> and how we as a project take these annotations and maintained them.
>
> I see on the Frama-C website Linux is supported and so I decided see how
> FreeBSD
> goes. I installed ocaml for FreeBSD as a result of some configure errors with
> ..
>
> $ pkg install ocaml ocaml-findlib
>
> however configure returned ...
>
> checking for ocamlgraph... ocamlfind: Package `ocamlgraph' not found
>
> This one package wants to install 118 packages some dependent on gnome,
> gnome-theme, docbook, gstreamer, bash and more so I have said no to installing
> them and I have decided to give up for now. The box I am using is a headless
> build server.
>
> Chris
--------------------------------------------------------------------
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@TCD, Head of Foundations & Methods Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------
_______________________________________________
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
