我正在尝试使用 Frama-C 值分析来研究生成的大型 C 代码,其中绑定(bind)检查是使用按位与 (&) 而不是逻辑与 (&&) 完成的。例如:
int t[3];
...
if ((0 <= x) & (x < 3))
t[x] = 0;
Frama-C 值分析提示数组访问:
warning: accessing out of bounds index [-2147483648..2147483647]. assert 0 ≤ x < 3;
我设法通过在测试前添加断言使其对小示例感到满意:
//@ assert (x < 0 || 0<=x);
//@ assert (x < 3 || 3<=x);
并增加 slevel
但我不能在实际代码中这样做(太大!)。
有人知道我可以做什么来移除这个警报吗?
(顺便说一句,是否有任何理由以这种方式编写测试?)
最佳答案
下面的补丁将使Value统一处理e1 && e1
和c1 & c2
,其中c1
和c2
是条件(但不是任意表达式)。
Index: src/value/eval_exprs.ml
===================================================================
--- src/value/eval_exprs.ml (révision 21388)
+++ src/value/eval_exprs.ml (copie de travail)
@@ -1748,11 +1748,23 @@
reduce_by_comparison ~with_alarms reduce_rel
cond.positive exp1 binop exp2 state
- | true, BinOp (LAnd, exp1, exp2, _)
- | false, BinOp (LOr, exp1, exp2, _) ->
+ | true,
+ ( BinOp (LAnd, exp1, exp2, _)
+ | BinOp (BAnd, (* 'cond1 & cond2' can be treated as 'e1 && e2' *)
+ ({ enode = BinOp ((Le|Ne|Eq|Gt|Lt|Ge), _, _, _)} as exp1),
+ ({ enode = BinOp ((Le|Ne|Eq|Gt|Lt|Ge), _, _, _)} as exp2),
+ _))
+ | false,
+ ( BinOp (LOr, exp1, exp2, _)
+ | BinOp (BOr, (* '!(cond1 | cond2)' can be treated as '!(e1 || e2)' *)
+ ({ enode = BinOp ((Le|Ne|Eq|Gt|Lt|Ge), _, _, _)} as exp1),
+ ({ enode = BinOp ((Le|Ne|Eq|Gt|Lt|Ge), _, _, _)} as exp2),
+ _))
+ ->
let new_state = aux {cond with exp = exp1} state in
let result = aux {cond with exp = exp2} new_state in
result
+
| false, BinOp (LAnd, exp1, exp2, _)
| true, BinOp (LOr, exp1, exp2, _) ->
let new_v1 = try aux {cond with exp = exp1} state
关于c - 如何让 Frama-C 在测试中理解按位 AND?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/14733696/