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

[Frama-c-discuss] About the status of assertions in dead code



Hello again,

Le 30/05/2013 13:34, Anne Pacalet a ?crit :
> What can we say about the status of an assertion at a program point
> that is detected as dead code by Value ?
> Would it be ok (I mean consistent with everything else) to mark it
> as Valid ? or should there be another special status ?

As someone nicely pointed out, the answer is in the documentation :
http://frama-c.com/download/frama-c-user-manual.pdf p35

Very sorry for the noise: I should have checked before of course... :-/

--
Anne.