Software Reports

[droter]

The ROS Safety group suggested adding another test to HAROS (https://github.com/git-afsantos/haros):

• Bounded Model Checker for C and C++ programs - https://www.cprover.org/cbmc/

Is the idea to extend HAROS with safety and security tests? Or does each group make their own report?

[afsantos]

I approve the idea of adding CBMC to HAROS. It provides many useful checks on its own, but, if I remember correctly, sometimes you might have to annotate your programs with a few assertions and assumptions to get additional benefit.

I am also curious as to how people would like to approach this integration (running only a few standard checks versus something more customized).