PR# 18945 Not properly joining pre & postcondition on select and join
Problem Report Summary
Submitter: mischael
Category: Compiler
Priority: Medium
Date: 2014/08/26
Class: Bug
Severity: Non-critical
Number: 18945
Release: 14.05
Confidential: No
Status: Analyzed
Responsible:
Environment: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Firefox/31.0
Synopsis: Not properly joining pre & postcondition on select and join
Description
When two features with the same origin are joined, or one is selected, it is possible to select one that has a weaker postcondition than the other. The program will then dynamically bind the feature including the weaker postcondition. Therefore the static precondition can be stronger than the dynamic. The same is true for the precondition, where the static precondition can be weaker than the dynamic. The expectation would in both cases be that the preconditions are or'd and the postcondition and'd.
To Reproduce
See the attachment for an example of both problems (join and select)
Problem Report Interactions
You are right that the compiler does not do the right thing because when merging 2 routines it keeps the body of the selected version as is included its contracts but the contracts as seen in the parents not the descendants because the code is not replicated. However, although not formalized yet, it is most likely that the compiler will now reject joining of 2 routines if one of them is kept as is, it will now force you to redefine the body of the routine so that you have a chance to provide an implementation that will satisfy any of the merged preconditions and of course ensures all merged postconditions. When this is implemented, we will close this bug report. In the meantime, make the redefinition manually when you do such a merge.