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