frama-c能否获取特定程序代码前的变量范围

Question

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*/

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

Answer 1

如果我理解你的问题，你想知道 A 在特定语句的变化区间。我假设您依赖于 Eva 插件，因为它是 Eva 通常提供的那种信息（至少如果我解释得很好 "instead of the range of A at the end of the program execution"）。

有两种可能。第一个是使用 Eva 的程序化 API，即 Db.Value 模块。这需要了解 OCaml 并阅读 Frama-C developer manual，但这是访问信息的最灵活和稳定的方式。简而言之，Db.Value.get_state 将 return 在 Eva 分析器的运行之后计算的抽象状态，用于作为参数给出的语句，而 Db.Value.eval_expr，将给定一个抽象状态和一个表达式，计算相应状态下表达式的抽象值。

第二种可能性是使用 Frama_C_show_each_* 系列内置函数：每当 Eva 遇到名称以 Frama_C_show_each_ 开头的函数时，它将在标准输出上打印抽象值当前抽象状态下赋予函数的参数。因此，在调用 task(A) 之前添加 Frama_C_show_each_A(A); 将为您提供 frama-c -eva test.i，以及其他

[eva] test.i:19: Frama_C_show_each_A: [1..2147483647]

请注意，我已经修改了您的代码以使其运行与 Frama-C 正确搭配：

添加了原型 extern int rand(void); 和 extern void task(int);
添加了一个“;”在 task(A)

请确保您提供 a minimal, complete and verifiable example with your questions，这使他们更容易回答

frama-c能否获取特定程序代码前的变量范围

Whether frama-c can get the range of variables before a particular program code

c

frama-c