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