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 Feb 4 11:43:27 2011  
Category: DevelopmentModule: BCaml/Bgop
Priority: 7 - HighSeverity: 4 - Important
Status: ConfirmedPrivacy: Public
Assigned to: Samuel Colin <scolin>Open/Closed: Open

Sat Feb 5 10:22:02 2011, 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 Feb 4 11:43:27 2011, 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 :
... & ( essai_possible = bool ( nbess < 3 ) )

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

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.


    Error: not logged in



    Follow 3 latest changes.

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

    Back to the top

    Powered by Savane 3.1-cleanup