4

Frama-C値分析を使用して、論理積（&&）ではなくビット単位のAND（＆）を使用して境界チェックが行われる大規模な生成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。ここで、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
于 2013-02-06T17:12:56.373 に答える
1

その例では、の両側&がすでに0または1であるため、その場合は&代わりにを使用しても問題ありません&&。

そのようにテストを書く理由はありますか

いいえ、彼らが故意にそうする理由は考えられません。&一般に、コードが後で変更され、一方の側が0-1値でなくなった場合、コードが破損するため、これは悪い考えです。

次に、実際の問題について説明します。

int t[3];また、複数回（たとえば、{}内）生成されますか、それとも1回だけ生成されますか？一度だけ定義された場合、問題の解決策はそれをmallocすることですint* t = malloc(3*sizeof(int))。コンパイラはもはや文句を言いません。

于 2013-02-06T16:28:13.500 に答える