Hacker News Reader

Comment by unwind | Hacker News Reader

This:

C's semantics also makes a lot of things which I would assume was "trivially true" fail verification. This isn't Frama-C's fault however, of course.

sounds really interesting, do you remember some concrete example? Not saying you're wrong or anything, just curious of what kind of code is hard to analyze like this.

View on HN

I was wondering about this too. If I was going to guess I would say it could be stuff that applies to any language that uses fixed width machine types, and not only C. For example, this is not true:

  ∀a: a+1 > a

if the type of 'a' is 32 bit int. Similarly negate(a) ≠ -a for some numbers.

Note that it's especially nasty in C, because it's either true or undefined behavior due to signed integer overflow.

Having written test cases for a similar semantic program analysis tool, I agree: Integer overflow is a very likely cause for such "obviously correct but actually wrong" program invariants. The C semantics can make this problem even worse since signed integer overflow is undefined, leaving the user of such a framework to the mercy of the design decisions of the creators of the framework regarding undefined behavior.

Right, that makes total sense yes. Thanks.

could you add some modifier?

"iff a =/= MAXINT"

In SPARK/Ada you'd have to constrain the input for something like that or it wouldn't be able to discharge the proof. Suppose you wanted a simple function (which is too simple to write in reality, but for brevity):

  function Increment(A : Integer) return Integer
    with Post => Increment'Result = A + 1;

It would find the counterexample for the situation where A is equal to Integer'Last. So you'd need to add a precondition like:

  function Increment(A : Integer) return Integer
    with Pre => A < Integer'Last,
         Post => Increment'Result = A + 1;

(doing this from memory and not fluent, so syntax may be off but the idea isn't)

You can do that in Frama-C as well. But now this new precondition must be propagated somewhere. For example, if you have some function (syntax from memory as well):

    /*@ ensures \result > a; */
    int increment(int a) {
        return a + 1;
    }

you would change it to:

    /*@ requires a < INT_MAX;
        ensures \result > a; */
    int increment(int a) {
        return a + 1;
    }

But if this function has N call sites, you now have N problems: At every call site you must prove that the precondition holds.

Frama-C has a wp plugin that generates assertions about overflow and underflow, which is one of the best tools it has. It's not spectacular about telling you where the problem is, and wasn't great with floats, though.

Complicating it even more, if "a" is a signed-integer than the compiler will assume that statement holds and optimize accordingly, put your correctness prover would instead need to flag that (or add the caveat that a < INT_MAX)

If I remember correctly, in ANSI C int is guaranteed to have the maximum value of only 65,535 when unsigned, so basically bounds checking is a must. Of course it's even more important for shorter types like char.

Reply on news.ycombinator.com