--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on March 2009 ---
> 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