c - frama-c是否可以在特定程序代码之前获取变量范围

int main()
{
    int B = 1;
    int x = rand()%10+1;
    int x1 = rand()%10+1;
    int A = 1;
    while((B <= 5))
    {
            B++;
            A++;
            if(B == x)
            {
                return 0;
            }
    }
    task(A) //The variable A passes in the range of values before the task function
    A = -2;
    return 0;
}
/*How can I use frama-c to get the range of A at task code if I want to get the range of A at task statement position instead of the range of A at the end of the program execution*/

如果我想在程序执行结束时获取at任务语句位置的范围而不是A的范围，那么如何使用frama-c来获取at任务代码的范围

最佳答案

如果我能很好地理解你的问题，你想知道在一个特定的陈述中A的变化间隔。我假设您依赖于Eva插件，因为它是Eva通常提供的信息类型（至少如果我解释得很好，“而不是程序执行结束时的A范围”）。
有两种可能性。第一种是使用Eva的编程API，即Db.Value模块。这需要了解OCAML和阅读Frama-C developer manual，但它是最灵活、最稳定的访问信息的方式。简而言之，Db.Value.get_state将返回Eva分析器运行后计算的抽象状态，对于以参数形式给出的语句，而Db.Value.eval_expr将在给定抽象状态和表达式的情况下，在相应状态下计算表达式的抽象值。
第二种可能是使用内置函数的Frama_C_show_each_*系列：每当Eva遇到一个名称以Frama_C_show_each_开头的函数时，它将在标准输出上打印当前抽象状态下给该函数的参数的抽象值。因此，在调用Frama_C_show_each_A(A);之前添加task(A)将给您带来
frama-c -eva test.i
请注意，我已经修改了您的代码，以便让它在Frama-C中正常运行：
增加了原型[eva] test.i:19: Frama_C_show_each_A: [1..2147483647]和extern int rand(void);
在extern void task(int);
请确保您提供a minimal, complete and verifiable example with your questions，这使他们更容易回答

关于c - frama-c是否可以在特定程序代码之前获取变量范围，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/53589688/