--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on February 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Value Analysis] multi state propagation



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.