Frama-C: Modular Analysis of C Programs

Re:Frama-C: Modular Analysis of C Programs by Jtsummers on Tuesday October 06, 2020 @11:20AM (#24698607)

The loop invariants that you can detect may not be the loop invariants that they want. Consider:

  for(int i = 0; i < n; i++) {..}

It looks like the invariant should be:

  0 <= i < n

But if they mistyped the loop that would be wrong. You have to explicitly state your invariants. At best, you could detect them and ask for confirmation. And that's for an easy to detect case.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by im3w1l on Tuesday October 06, 2020 @12:01PM (#24699161)

This sounds like an invariant even an optimizing compiler could find, because it's such a common construct. Well... I guess they have an easier job because they can "assume away" signed overflow.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by Jtsummers on Tuesday October 06, 2020 @12:14PM (#24699334)

My point was that that may not be the actual invariant. By making your invariants explicit these tools have a better chance of finding real errors since you compare the code against a specification. Deriving a specification just means your code works according to itself.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by mcguire on Tuesday October 06, 2020 @12:26PM (#24699533)

Presumably, you are doing something other than just incrementing i in the loop, though.

Most of the time with Frama-C, all you have to provide is function pre- and post-conditions and loop invariants.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by the-smug-one on Tuesday October 06, 2020 @11:36AM (#24698830)

What programs can do is "loop invariant synthesis" (for people that want to google it), this is still quite tricky to do. There's a reason that humans also find loop invariants tricky.

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by KsassPeuk on Wednesday October 07, 2020 @03:03AM (#24705958)

In fact that would be

``` 0 <= i <= n ```

As the loop reaches this value to terminate. Else, we could not deduce for example that `i = n` at the end of the loop (`0 <= i <= n && !(i < n)`).

[ Parent | on HN ]