Search code examples
cframa-c

How to make Frama-C understand bitwise AND in tests?

I am trying to use Frama-C value analysis to study a large generated C code where the bound checks are done using a bitwise AND (&) instead of a logical AND (&&). For instance:

int t[3];
...
if ((0 <= x) & (x < 3)) 
  t[x] = 0;

Frama-C value analysis complains about the array access :

warning: accessing out of bounds index [-2147483648..2147483647]. assert 0 ≤ x < 3;

I managed to make it happy on small examples by adding assertions before the test:

//@ assert (x < 0 || 0<=x);
//@ assert (x < 3 || 3<=x);

and increasing the slevel but I can't do that in real code (too large !).

Does anybody have an idea of what I can do to remove this alarm ?

(BTW is there any reason to write the tests that way ?)

Solution

  • The patch below will make Value deal uniformly with e1 && e1 and c1 & c2, where c1 and c2 are conditions (but not arbitrary expressions).

    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