Type check and code pattern detection, Frama-C

Question

I'm discovering the Frama-C software and I was wondering if it is possible to detect some code pattern such as a doubled if tests or for example that a call to a given function is always followed by another.

Or maybe somethings using the variables names, like for instance check if a variable with a given prefixed named belongs to a certain type.

Do you think it's possible with Frama-C (using ACSL or by developing a new module) ?

Thanks a lot =)

Answer 1

to detect some code pattern such as a doubled if tests

if you mean a pattern in which the condition of the inner if is always true because it is a consequence of the outer if, the GUI can already show you that the inner if's else branch has been found to be unreachable during the value analysis.

For a simple example:

int x, y;

int main(int c){
  if (c == 2)
    {
      x = x * c;
      if (c == 2)
        {
          y = y * c;
        }
      else
        {
          y = y / c;
        }
    }
}

The commandline is:

$ frama-c-gui -val t.c

This can be used heuristically only. A sound detector for redundant tests separated by an execution path along which the variables involved have not been modified could be implemented as a plug-in taking advantage of the value analysis' results.

that a call to a given function is always followed by another.

This is possible using Aoraï, a Frama-C plug-in that is (EDITED:) included in the Frama-C distribution despite what its webpage claims. Aoraï generates proof obligations that correspond to the temporal property that has been expressed. Proving these obligations may be more or less difficult. In a way, Aoraï only reduces the problem of verifying temporal properties to another problem for which there are plug-ins in Frama-C.

check if a variable with a given prefixed named belongs to a certain type.

This type of “coding standard” check can be implemented as a Frama-C plug-in too. Atos implemented a plug-in named Taster to verify Airbus coding rules.