--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on July 2012 ---
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