Вычисление сводки функций с использованием анализа значений Frama-C

Question

Допустим, у нас есть следующий пример кода:

int a(int x){
    if (x < 0){
        return -50;
    }
    if (x >= 0 && x <= 3600){
        return x - 100;
    }

    return x + 100;
}

int main(){
    int q = Frama_C_interval(50, 5000); 

    return a(q);
}

Запустив инструмент анализа значений frama-c, я могу определить интервал результата a(), который, как и ожидалось, равен [-50, 5100]. То, что я хотел бы вычислить сейчас, - это краткий обзор функции (), то есть отношения между входом и выходом. Результат, который я ищу в приведенном выше примере, будет выглядеть примерно так:

[50,3600] -> [-50, 3500]
[3601,5000] -> [3701, 5100]

Обратите внимание, что меня интересует контекстное резюме, поэтому другие случаи в функции a() представляют меньший интерес.

Каков был бы лучший способ достичь этого?