--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on July 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] value analysis



Hello,

I think your C-statements are easier to understand (and your question easier to answer)
if you present them as part of a small C-function together with the ACSL contract you tried.

Regards

Jens

On 8 Jul 2012, at 01:16, Drew Shaw wrote:

I am trying to get frama-c to perform a value analysis on n_start.  I have tried using axioms to tell frama-c that n_start greater than or equal to (start - 31) and less than or equal to start.  Perhaps I am not taking the right approach can someone help?
uint32_t start, n_start;
n_start = 0;
start = Frama_C_interval (0, CHAR_MAX);
n_start = start - start%32;
_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr>
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss