我正在尝试使用 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，但我无法在实际代码中做到这一点（太大了！）。
有人知道我可以做些什么来消除这个警报吗？
（顺便说一句，有什么理由这样写测试吗？）
【问题讨论】：
下面的补丁将使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
【讨论】：
在该示例中，& 的两边已经是 0 或 1，因此在这种情况下使用 & 而不是 && 是可以的。
有什么理由这样写测试
不，我想不出他们会故意这样做的任何理由。一般来说，这是一个坏主意，因为如果稍后更改代码并且& 的一侧不再是 0-1 值，那么代码就会中断。
现在是实际问题：
int t[3]; 是否也多次生成（例如在 {} 中）还是仅生成一次？如果它只定义一次，那么解决问题的方法是对其进行 malloc：int* t = malloc(3*sizeof(int))。编译器将不再抱怨。
【讨论】：
((0 <= x) & (x < 3)) 是一个有效的 0
t 指向一个大小为3 个整数的malloc 分配块时，t[x] 是一个有效的内存访问并不比t 是一个数组时更明显，所以使用malloc 不会绕过任何检查。只要 Frama-C 看不到 0 ≤ x t[x]。