--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on March 2019 ---
Hello everyone! I'm a student doing my master thesis in deductive verification and I am using Frama-C as a part of it. During my work with Frama-C I have encountered some interesting behaviour which have left me puzzled and I would greatly appreciate it if you could provide me with some answers. My first question relates to the use of the ternary operator (? :) and the assigns-clause. It seems like using a ternary expression within an if-else statement sometimes leads to some assigns-clauses being unprovable, replacing the ternary with something equivalent solves the problem. I am adding an example showcasing this behavior between the dashed lines. The code that I have been verifying is proprietary so this code is just an example, but it follows some of the same coding rules which is why it might look unusual. Would I be correct in assuming that this is a bug? Or is there some other explanation for what is happening? ----------------------------------------------- typedef unsigned char bool; typedef unsigned char u08; #define TRUE ((bool)1) #define FALSE ((bool)0) // Original define ==> unprovable assign. #define IS_MAX(ss_U08) ( (((ss_U08) & (0xFF)) == (0xFF) ) ? (TRUE) : (FALSE)) // Without the bit-and ==> unprovable assign. // #define IS_MAX(ss_U08) ( ((ss_U08) == (0xFF)) ? (TRUE) : (FALSE)) // Can prove everything // #define IS_MAX(ss_U08) ((bool)(ss_U08 == 0xFF)) /*@ requires \separated(p,b,c); ensures (IS_MAX(*b) == TRUE && IS_MAX(*c) == TRUE) ==> *p == 3; ensures (IS_MAX(*b) == TRUE && IS_MAX(*c) == FALSE) ==> *p == 2; ensures (IS_MAX(*b) == FALSE && IS_MAX(*c) == TRUE) ==> *p == 1; ensures (IS_MAX(*b) == FALSE && IS_MAX(*c) == FALSE) ==> *p == 0; assigns *p; */ void foo(u08* p, u08* b, u08* c){ if(IS_MAX(*b) == TRUE && IS_MAX(*c) == TRUE){ *p = 3; }else if(IS_MAX(*b) == TRUE && IS_MAX(*c) == FALSE){ *p = 2; }else if(IS_MAX(*b) == FALSE && IS_MAX(*c) == TRUE){ *p = 1; }else{ *p = 0; } } ---------------------------------------------- For my second question, I was wondering if I could get an explanation as to how switch-cases are handled in Frama-C? I've noticed that the post-conditions for a function with a switch-case are split into N parts, with N being the number of cases present in the switch. The switch-cases present in the code I am verifying have breaks at the end of every case and so should be equivalent to an if-else statement. However, this splitting behavior causes the verification time for a function with switch-cases to be much larger than the same function with an if-else replacing the switch-case. So i was wondering why is there such a difference between the two? Thank you for your time, Erik Söderberg -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190307/0392199d/attachment.html>