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 and user-defined predicates

Hi,

On Tue, Apr 10, 2012 at 3:04 PM, sylvain nahas
<sylvain.nahas at googlemail.com> wrote:
> I would expect the status "valid" for all "assert" above, but the
> value analysis obstinately considers the second one as "unknown".

The fragment of ACSL understood by the Value Analysis is limited,
albeit evolving towards increased support. Some great progress have
been made between Carbon and Oxygen: ranges and many other things in
Nitrogen, \separated and improved \initialized in Oxygen, etc.
However, user-defined predicates are currently not handled, and won't
be in Oxygen. Depending on our available time, they _may_ be present
in Fluorine.

HTH,

-- 
Boris