RTEMS qualification and code annotations

[Chris Johns]

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