--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on November 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] NON TERMINATING FUNCTION when adding specification



Hi Boris,

Le 16/11/2012 12:11, Boris Yakobowski wrote :
> I suspect that in the analysis with the 'ensures' clause, you also get a
> message "postcondition got status invalid", which indicates that Value's
> analysis cannot continue (by lack of memory state after the post).

Yes.

> The problem here is an instance of the one you had in your message of
> 2012-04-12, so I'm just going to refer you to it.

I will carefully re-read it again since it is not obvious for me
at the moment that it is the same problem...

> In the meantime, we have added support for \null,
> and the problem-to-come in Oxygen has been solved,

This remark is also related to my problem ?
It seems to me that nothing is \null here, since the pointer is an array...

> so everything should ultimately work as you expect.

Great !

And thank you very much for your answer.
-- 
Anne.