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: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Thu, 7 Mar 2019 17:00:47 +0100
  • In-reply-to: <1551971500735.70991@kth.se>
  • References: <1551971500735.70991@kth.se>
Hello,

Le jeu. 7 mars 2019 à 16:12, Erik Söderberg <esoderb at kth.se> a écrit :

>
>
> 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?
>

Yes, this looks very much like a bug. Based on a quick inspection of WP's
results on your example, it apparently fails to see that an assignment to a
temporary variable generated by the expansion of the ternary operator is an
assignment to a local variable and should not invalidate the assigns
clause. At the very least, this warrants further investigation from our
side. Thanks for the report!


> 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?
>

I can't directly answer to this question as it depends on the innermost
part of WP, but you can ask the kernel to replace the switches by
equivalent if else statements with the -simplify-cfg option.

Note in addition that splitting the proof obligations is sometimes
necessary: if you have really many possible execution path in a single
function, provers might have some difficulties coping with everything at
once. In that case, -wp-split (which can be activated on a case-by-case
basis through a checkbox in the GUI) will give you the possibility to split
the overall proof obligation into smaller, more palatable pieces.

Best regards,

-- 
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190307/fa7fa77e/attachment.html>