> I'm simply saying that for the restricted case of safety semantics alone, this deduction can be done.

And I'm saying it can't be done, at least not in a fundamentally less tedious and hard way than Frama-C.

> Yes, it is impossible to deduce semantic equivalence of arbitrary functions. The question is whether it is possible to deduce that annotations capture the safety semantics of the body.

It isn't in general.

> If you have a concrete example it would be helpful here – but for the restricted concerns of safety, not for arbitrary constructs.

Safety is not a "restricted concern": You can for every property P easily construct a function that is safe if and only if property P holds. I'll be using Python because this example (which I like) requires arbitrary size integers. You could obviously also implement this in C, you'd just need to implement arbitrary size integers (or use a library that implements them):

    def collatz(x):
        if x % 2 == 0:
            return x // 2
        return x * 3 + 1

    def cycle(f, x):
        tortoise = f(x)
        hare = f(f(x))

        while tortoise != hare:
            tortoise = f(tortoise)
            hare = f(f(hare))

        return hare

    buffer = [0, 0, 0, 0, 0]
    x = int(input())
    if x >= 1:
        collatz_cycle_element = cycle(collatz, x)
        print(buffer[collatz_cycle_element]) # this is safe (or is it?)

This takes as an input an arbitrary positive integer x, searches for a cycle in the Collatz sequence beginning with that number and returns an arbitrary element of that cycle. It is conjectured that for every positive integer this cycle will be 4 -> 2 -> 1 -> 4 -> ... and thus this program is safe if and only if the Collatz conjecture holds.

Another example would be a C program that generates random planar graphs, computes their chromatic numbers and then collects statistics about them in an `int statistics[5]`:

    #include <stdio.h>

    void main() {
        int statistics[5] = {0};

        for(int i = 0; i < 1000; i++) {
            struct graph g = generate_random_planar_graph();
            int chromatic_number = compute_chromatic_number(g);
            statistics[chromatic_number] += 1;
        }
        
        printf("%i, %i, %i, %i", statistics[1], statistics[2], statistics[3], statistics[4]);
    }

The safety of this program requires you to prove that `generate_random_planar_graph` always returns a planar graph, that `compute_chromatic_number` correctly identifies the chromatic number and that the chromatic number of every planar graph is less than 5.