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

[Frama-c-discuss] Proving a simple property on bitshift with WP



Hello Dillon,

2013/8/29 Pariente Dillon <Dillon.Pariente at dassault-aviation.com>:
> Coupling Value and WP to the extensive annotations below (discharged by Value) also allows to discharge the last assert by WP.

Thanks a lot for this solution!

> (This is a very verbose solution, indeed, but might be still readable)

This is verbose indeed but at least the verbose part is in the
annotations and I don't need to modify the program, which is much
better.

Best regards,
david