---
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
- Subject: [Frama-c-discuss] Proving a simple property on bitshift with WP
- From: dmentre at linux-france.org (David MENTRE)
- Date: Wed, 11 Sep 2013 09:10:48 +0200
- In-reply-to: <835769EB-9F81-4D66-B430-6C2AF8C6BF46@cea.fr>
- References: <CAC3Lx=YN+ofoawh_vint2WumaAd6=akQaLccmrg8BV6wBOphmA@mail.gmail.com> <CA+yPOVj2PgA5gtp-OhSgeNumhmvOmmtM78KNBcVTtBXdzJeAZg@mail.gmail.com> <CAC3Lx=b2ngvaheSxzLr=5ZZi_R1T4fym7uYOW1yV3ARg0QRY-w@mail.gmail.com> <1A32855E5FA08141A8C56E7CF24D442C0EFD8A23@SCTEX101.st-cloud.dassault-avion.fr> <CAC3Lx=YhKt+5FGwwG1cmuFZxQm67QNeRPXmxtnYDqHmTpR189g@mail.gmail.com> <835769EB-9F81-4D66-B430-6C2AF8C6BF46@cea.fr>
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