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] [Value Analysis] multi state propagation

  • Subject: [Frama-c-discuss] [Value Analysis] multi state propagation
  • From: anne.pacalet at free.fr (Anne Pacalet)
  • Date: Wed, 06 Feb 2013 17:34:37 +0100
  • In-reply-to: <CABbVA-Dsgnj5bNEn-TGpDc7=XAFRZ2pBYbKVsRfDxRwWXpHuqA@mail.gmail.com>
  • References: <51078966.40703@free.fr> <CABbVA-Dsgnj5bNEn-TGpDc7=XAFRZ2pBYbKVsRfDxRwWXpHuqA@mail.gmail.com>
Hi Boris,

First of all, thank you for your clear explanation that
confirmed what I guessed.

Le 06/02/2013 17:16, Boris Yakobowski a ?crit :
> The feature you would like, specifying (typically through ACSL
> disjunctions) that some states must remain separate during analysis,
> has been under consideration for quite some time now. It is indeed the
> next step logical step after -val-split-return-function.

I am happy to know that I am not the only one who would like this feature,
but I also understand from what you said that this would require
a large amount of work.

> Unfortunately, we are unlikely to find the time to implement such an
> invasive change without a collaborative project.

Ok, I can understand that.

Thanks again.
-- 
Anne.