Traceability from specification to source code?

[Chris Johns]

On 2020-03-31 05:52, Sebastian Huber wrote:
> Hello Gedare,
> 
> On 30/03/2020 18:17, Gedare Bloom wrote:
>> This question is related to
>> https://lists.rtems.org/pipermail/devel/2019-September/055519.html
>> about code annotations, and similar discussion raised there applies
>> here.
> 
> thanks for referencing this thread. Unfortunately, the outcomes of this 
> thread are not written down in the Software Engineering Manual 
> (definitely our fault). I read the thread again, but I think the 
> situation here is a bit different.
> 
> For the traceability between source code and the specification we likely 
> don't need additional complex third-party tools (I depends a bit if we 
> want to use a C statement as a scope for an annotation for example, but 
> this is more a comfort feature). Also in contrast to the annotations for 
> the formal methods tools, the link annotations are simple and you don't 
> need expert knowledge to understand them.

I think the 3 major headings Joel listed are valid, that is Annotation, 
Supporting Tools, and Maintenance.

How smart is the scanner used to extract these strings and how resilient 
is the expected qual out come to localised changes in the code around 
these label? I have looked at your example for a while now to determine 
the relationship between the opening label and the default value and it 
seems complex to me and I would not like to be making changes around 
this area without either a clear understanding of what is happening or a 
disregard for the quality of the qual information. I do not like either 
of these options. Add to this the C language can be rather tricky to 
parse at the best of times.

How do we limit what can be added? Joel refers to this as 
"Invasive/Intruding/Bulk". We currently have doxygen, we then add this 
and then maybe Frama-C, i.e. signal-to-noise ratio starts to make seeing 
the actual code hard.

> The formal methods support is 
> optional for a pre-qualification and only required for higher 
> criticality categories. The traceability, however, is a basic 
> requirement of the standards. This is something we have establish, 
> otherwise there will be no RTEMS Qualification project at all.

I would like to understand what the requirement for traceability is you 
need to satisfy? In your example is it to know the definition, i.e. 
file:line, for..

  CONFIGURE_MAXIMUM_BARRIERS
  _Objects_.*_Barrier_.*      (A guess at expanded label)

?

Have you considered a gcc plugin [1] or some other compiler generated 
data format that contains this detail, ie DWARF? In other words, are you 
adding tags and related detail because parsing the C code is hard? Or I 
am mistaken in assuming the compiler sees and understands all this 
stuff? I am assuming it has to by definition or there is not need to 
track it?

Chris

[1] https://github.com/davidmalcolm/gcc-python-plugin