--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie regions



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
>