bugBRILLANT - Bugs: bug #17645, bbool decompilation

 
 
Show feedback again

You are not allowed to post comments on this tracker with your current authentification level.

bug #17645: bbool decompilation

Submitted by:  Georges Mariano <gmariano>
Submitted on:  Fri 04 Feb 2011 11:43:27 AM UTC  
 
Category: DevelopmentModule: BCaml/Bgop
Priority: 7 - HighSeverity: 4 - Important
Status: ConfirmedPrivacy: Public
Assigned to: Samuel Colin <scolin>Open/Closed: Open

Sat 05 Feb 2011 10:22:02 AM UTC, comment #1:

From the look of it, it seems that I forgot to unfold the bool construct when it appears in a predicate/expression, this action should be done in the bgop.

This is the reason why I put this comment in the XSLT : this substitution-like construct should never appear in a calculated proof obligation.

A failure on my part in the code of the BGop, I reassign it to the Bgop module.

I also note here to document the algorithm of the unfolding of this construct when only used in expressions/predicates (it is already more or less documented in the BBook when used in a substitution, if I remember well).

Samuel Colin <scolin>
Project AdministratorIn charge of this item.
Fri 04 Feb 2011 11:43:27 AM UTC, original submission:

bicoax run fail with messages like the following :

The term "_nbess < 3" has type "Prop" while it is expected to have type "bool".

COQ.v context :
Forall [...], (
(In (interval 0 9999) _code_saisi) ->
(In BBOOL _etat_clc) ->
(In BBOOL _essai_possible) ->
(In (interval 0 3) _nbess) ->
...
(_essai_possible = ((_nbess < 3))) ->
...

SPEC.imp context :
INVARIANT
... & ( essai_possible = bool ( nbess < 3 ) )

XSLT :
<!-- SC: normally this tag should never appear. Left for compatibility -->
<xsl:template match="BoolEvaluation">
<xsl:apply-templates select="child::*"/>
</xsl:template>

Georges Mariano <gmariano>
Project Administrator

 

No files currently attached

 

Depends on the following items: None found

Items that depend on this one: None found

 

Carbon-Copy List
  • -unavailable- added by scolin (Posted a comment)
  • -unavailable- added by gmariano (Submitted the item)
  •  

    Do you think this task is very important?
    If so, you can click here to add your encouragement to it.
    This task has 0 encouragements so far.

    Only logged-in users can vote.

     

    Please enter the title of George Orwell's famous dystopian book (it's a date):

     

     

    Follow 3 latest changes.

    Date Changed By Updated Field Previous Value => Replaced By
    Sat 05 Feb 2011 10:22:02 AM UTCscolinModuleBiCoax=>BCaml/Bgop
      Severity3 - Normal=>4 - Important
      StatusNone=>Confirmed
    Show feedback again

    Back to the top


    Powered by Savane 3.1-cleanup