c - 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] であることが判明しました。ここで計算したいのは、a() の関数の要約、つまり入力と出力の関係です。上記の例で探している結果は、次のようになります。

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

私はコンテキストベースの要約に興味があるので、関数 a() の他のケースはあまり興味がないことに注意してください。

これを達成するための最良の方法は何ですか？