xen-analysis ECLAIR support

[Stefano Stabellini <sstabellini@xxxxxxxxxx>]

Hi Luca,

We are looking into adding ECLAIR support for xen-analysis so that we
can use the SAF-n-safe tags also with ECLAIR.

One question that came up is about multi-line statements. For instance,
in a case like the following:

diff --git a/xen/common/inflate.c b/xen/common/inflate.c
index 8fa4b96d12..8bdc9208da 100644
--- a/xen/common/inflate.c
+++ b/xen/common/inflate.c
@@ -1201,6 +1201,7 @@ static int __init gunzip(void)
     magic[1] = NEXTBYTE();
     method   = NEXTBYTE();
 
+    /* SAF-1-safe */
     if (magic[0] != 037 ||
         ((magic[1] != 0213) && (magic[1] != 0236))) {
         error("bad gzip magic numbers");


Would SAF-1-safe cover both 037, and also 0213 and 0213?
Or would it cover only 037?

We haven't use SAFE-n-safe extensively through the codebase yet but
my understanding is that SAFE-n-safe would cover the entire statement of
the following line, even if it is multi-line. Is that also your
understanding? Does it work like that with cppcheck?


It looks like ECLAIR requires a written-down number of lines of code to
deviate if it is more than 1 line. In this example it would be 2 lines:

     /* SAF-1-safe 2 */
     if (magic[0] != 037 ||
         ((magic[1] != 0213) && (magic[1] != 0236))) {

One option that I was thinking about is whether we can add the number of
lines automatically in xen-analysis based on the number of lines of the
next statement. What do you think?

It seems fragile to actually keep the number of lines inside the SAF
comment in the code. I am afraid it could get out of sync due to code
style refactoring or other mechanical changes.

Cheers,

Stefano