Frama-C: Modular Analysis of C Programs

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

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)

[ Parent | on HN ]

Re:Frama-C: Modular Analysis of C Programs by tom_mellior on Tuesday October 06, 2020 @12:46PM (#24699799)

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.

[ Parent | on HN ]