--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on July 2012 ---
Hello Drew, 2012/7/8 Drew Shaw <darwin401 at gmail.com>: > 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; > I think that you have to keep in mind that Frama-C's value analysis is non-relational. Thus, it can in the general case only check and/or take advantage of properties of a single variable (which "n_start is greater than or equal to (start - 31)" obviously isn't). According to some Value Analysis experts, the Only True Way?[1] to get past this point is to use -slevel, with appropriate ACSL disjunctions to separate the initial state in an useful manner.. Depending on what you're trying to achieve, this might be sufficient or not. For instance, with the attached script (for Nitrogen. Use like this: frama-c -load-script shaw_example.ml shaw_example.i) to generate the disjunction and set the slevel accordingly, Value analysis can decide that the assertion at the end of main in shaw_example.i is valid. Best regards, -- E tutto per oggi, a la prossima volta Virgile [1] http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2012-May/003234.html -------------- section suivante -------------- Une pi?ce jointe autre que texte a ?t? nettoy?e... Nom: shaw_example.i Type: application/octet-stream Taille: 208 octets Desc: non disponible URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120709/5dfd5390/attachment.obj> -------------- section suivante -------------- Une pi?ce jointe autre que texte a ?t? nettoy?e... Nom: shaw_example.ml Type: application/octet-stream Taille: 1073 octets Desc: non disponible URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120709/5dfd5390/attachment-0001.obj>