--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on March 2009 ---
Thank you very much Christoph ----- Original Message ----- From: "CUOQ Pascal" <Pascal.CUOQ at cea.fr> To: "Frama-C public discussion" <frama-c-discuss at lists.gforge.inria.fr>; "Frama-C public discussion" <frama-c-discuss at lists.gforge.inria.fr> Sent: Monday, March 09, 2009 10:51 PM Subject: Re: [Frama-c-discuss] Jessie regions >> referring the discussion regarding disjoint memory regions: > > I was hoping someone else would take up the gantlet, > but since no-one did, here I go. > >> I want to know, whether the built-in assumption that all >> memory regions are disjoint is a mere assumption or a precondition, > > In my previous answer, I divided the separation hypotheses > in two categories. > > 1/ The separation hypothesis that p is separated from &p is an > assumption. Jessie does not handle > such casts and although it is fundamentally a compositional > tool able to analyze a function outside of its context, it > still needs to assume that the context does not contain such > pointer casts that would break its memory model. One of these days > we are going to provide you with a methodology for insulating the > dangerous casts so that you can safely apply Jessie to some functions > even though dangerous casts are used in others. This is definitely > on our to-do list. Until then, the safest way is to restrict your use of > Jessie to applications that do not use unsafe casts *as a whole* -- > i.e. even outside the functions you are analyzing. > > 2/ The hypothesis that two distinct pointer arguments of a function > point to separate memory regions should be a precondition. It has been > a while since I last launched Jessie and I am not sure what it does now, > but if Jessie assumes the arguments pointers are separated, it certainly > should express the assumption it is making as a precondition. > > To sum up the answer to your question, it depends on the > category of the separation hypothesis. For category 1/, it's an > assumption. For category 2/, it should be a precondition. I am pretty > sure it is. It can not not be, can it? How could it? Yeah, it has to be > a precondition. > > Pascal > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >