--- layout: fc_discuss_archives title: Message 65 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



This point is not decided yet on our side.
But if you are interested in it, we may think about a more tied cooperation on these topics.
Regards,
	L.

Le 11 sept. 2013 ? 09:10, David MENTRE <dmentre at linux-france.org> a ?crit :

> 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
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss