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.