--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on February 2013 ---
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.