Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] value analysis

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>