2 ms·
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 we
by tom_mellior 6y ago
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.