--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on April 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Help with the Value Set Analysis



Hi,

I would like to know if is possible to see the interval-congruence values
(VSA) for the variables itself and not just
for the return statements. I will clarify my point by the log generated
using frama-c.

[value] ====== VALUES COMPUTED ======
[value] Values for function teste:
          a ? {1; 11; }
[value] Values for function Soma:
          __retres ? {10; }
[value] Values for function Subtrai:
          __retres ? [-10..8],0%2
[value] Values for function main:
          a ? {10; }
          b ? {0; }
          i ? {10; }
          soma ? {10; }
          subtracao ? {8; }
          __retres ? {1; }

Why is not shown that a and b for instance is coitained in the VSA [0,10].


I will appreciate with someone may clarity my question.

Thanks in advance,
Davidson
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100413/7d232323/attachment.htm>