--- layout: fc_discuss_archives title: Message 63 from Frama-C-discuss on September 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 Lo?c,

2013/9/2 Lo?c Correnson <loic.correnson at cea.fr>:
> Better support for bitwise operators in WP is an on-going work.
> Technically, we have to cope with the fact that SMT solvers are generally poor when mixing arithmetics and bitwise operations.
> Our working solution is to use, when needed, extended axiomatization for bitwise operators. The same observation applies to division and non-linear arithmetics.

Can we expect to have this better axiomatization for bitwise
operations in next release of Frama-C? I attempted to prove some
equivalence between two cryptographic codes and hadn't much success to
say the least. :-)

Best regards,
david