--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on June 2019 ---
Hi, I work on obfuscated C code and some operation have been reworked to made it hardly understandable. I had then to make them clearer for the different provers. I have proven that the operation 'a+b == (a&b) + (a|b)' for every 'int a' and 'int b' with '&' and '|' the bitwise operations. I then wanted every prover to "know" it and added it as an axiom. The issue is that I try to prove that 'a+b+c == (((a&b)+(a|b)) & c) + (((a&b)+(a|b)) | c)' but the provers can't reduce it with the axiom. Is there a way to make it understandable to provers ? (I can't add it directly as axiom too because the same problem will occur with 'a+b+c+d') Dorian. -------------- section suivante -------------- Une pièce jointe HTML a été nettoyée... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190611/3e509543/attachment.html>