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 _______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
