--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on April 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Value analysis] Validating a function with behavior spec.



Hi,

> 3) as Boris Hollas pointed out, an 'Unknown' status does not
> intrinsically indicate a deficiency in the analyzer.

For the record, I didn't suspected a deficiency in the analyzer but
rather in my understanding of how V.A. works. I was right with that.

> If you want to avoid those warnings, position your disjunction _before_ your
> ? ? ? ?/*@ assert ( in_int8 < 0 ) || ( in_int8 >= 0 ); */
> ? ? ? ?uint8 out_uint8 = abs8(in_int8);

So a "requires" in a contract hasn't the same effect?

> Hope this helps,

Yes, definitively.

Thank you very much.

Sylvain