Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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
>