--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on May 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Value Analysis] Interval Division



Hi,

We have a doubt.
We have a algorithm with some calculations in a loop and there is a
division between 2 variables that are intervals. We would like that the
result was 1 to variables with the same intervals, i.e., that the Frama-C
not compute the cartesian product. How to do that?

We ran some examples. In the example 1 with integer variables, it was easy
to employ asserts and get the correct results.

However the problem is with float variables. In the example 2, we have
tried to use similar asserts to example 1, but it did not work.

In the loop iterations of the algorithm, we are taking in account that:
-the intervals values are not constant
-the interval range can be large, the minimum value can be negative

example 1:

int test1, test2;
test1= Frama_C_interval(1, 5);
aux=(float)test1/(float)test1;

Frama-C output of example 1:
[value] Values for function main:
          aux ? [0.2 .. 5.]
          test1 ? {1; 2; 3; 4; 5; }

using the following assert in the example 1
//@ assert test1 > 0 &&  test1 < 2 || test1 > 1 &&  test1 < 3 || test1 > 2
&& test1 < 4 || test1 > 3 && test1 < 5;

Frama-C output of example 1 with assert:
[value] Values for function main:
          aux ? 1.
          test1 ? {1; 2; 3; 4; }

example 2:
float test1, test2;
float aux;
test1= Frama_C_float_interval(1.0, 5.0);
aux=test1/test1;

Frama-C output of example 2:
[value] Values for function main:
          test1 ? [1. .. 5.]
          aux ? [0.2 .. 5.]

Thanks a lot.
Rovedy, Nanci, Luciana
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130515/b9a5c9bf/attachment.html>