c - 如何让 Frama-C 在测试中理解按位 AND？

Question

我正在尝试使用 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 但我不能在实际代码中这样做(太大!)。

有人知道我可以做什么来移除这个警报吗？

(顺便说一句，是否有任何理由以这种方式编写测试？)

Answer 1

下面的补丁将使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