Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Issue with obfuscated C code

  • Subject: [Frama-c-discuss] Issue with obfuscated C code
  • From: dorian.dumanget at irisa.fr (Dorian Dumanget)
  • Date: Tue, 11 Jun 2019 14:34:33 +0200 (CEST)
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>