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 的范围
最佳答案
如果我很好地理解你的问题,你想知道 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_
开头的函数时,它将在标准上打印在当前抽象状态下输出给函数的参数的抽象值。因此,在调用 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 中正常运行:
- 添加了原型(prototype)
extern int rand(void);
和extern void task(int);
- 添加了一个';'在
任务(A)
之后
请确保您提供a minimal, complete and verifiable example with your questions ,这使他们更容易回答
关于c - frama-c能否获取特定程序代码前的变量范围,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/53589688/