ID0000689: **This issue was created automatically from Mantis Issue 689. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0000689 | Frama-C | Plug-in > Eva | public | 2011-01-26 | 2014-02-12 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | signoles | **Assigned To** | monate | **Resolution** | fixed | | **Priority** | normal | **Severity** | major | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 | ### Description : If a function has 1 valid ensure and 1 invalid ensure, the GUI says that both ensures are invalid. ### Steps To Reproduce : ==== a.c ==== /*@ ensures \result == 0; @ ensures \false; @ */ int f(void) { return 0; } void main(void) { f(); } ============== $ frama-c-gui a.c Then check the property status of both ensures.