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

  • Subject: [Frama-c-discuss] Jessie regions
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Mon, 9 Mar 2009 22:51:43 +0100
  • References: <7CD088A8-35C2-4166-AACB-C36086BBF58F@first.fraunhofer.de><EFEEF25A-DE4E-488A-B35F-064F5C4B614E@cea.fr> <7B29121BFC06467FA716CC00626745C6@AHARDPLACE>
> 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