4

我正在尝试使用 Frama-C 值分析来研究生成的大型 C 代码，其中边界检查是使用按位与 (&) 而不是逻辑与 (&&) 完成的。例如：

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但我不能在实际代码中做到这一点（太大！）。

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

（顺便说一句，有什么理由这样写测试吗？）

4

2 回答 2

4

下面的补丁将使 Value 统一处理e1 && e1and c1 & c2， where c1and c2are 条件（但不是任意表达式）。

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
于 2013-02-06T17:12:56.373 回答
1

在那个例子中，两边&都已经是 0 或 1，所以在这种情况下使用&代替&&是可以的。

有什么理由这样写测试吗

不，我想不出他们会故意这样做的任何理由。一般来说，这是一个坏主意，因为如果稍后更改代码并且一侧&不再是 0-1 值，那么代码就会中断。

现在到实际问题：

是int t[3];多次生成（例如在 {} 内）还是只生成一次？如果它只定义一次，那么解决问题的方法是对其进行 malloc: int* t = malloc(3*sizeof(int)). 编译器将不再抱怨。

于 2013-02-06T16:28:13.500 回答