--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on March 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Questions about ternary operator, assigns and switch-cases



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>