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