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() 中的其他情况不太感兴趣。

实现这一目标的最佳方法是什么？