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] Questions about ternary operator, assigns and switch-cases

  • Subject: [Frama-c-discuss] Questions about ternary operator, assigns and switch-cases
  • From: esoderb at kth.se (Erik Söderberg)
  • Date: Thu, 7 Mar 2019 15:11:41 +0000
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>