--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on September 2013 ---
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