ID0001978: **This issue was created automatically from Mantis Issue 1978. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001978 | Frama-Clang | Plug-in > clang | public | 2014-11-20 | 2015-02-16 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open | | **Priority** | normal | **Severity** | feature | **Reproducibility** | always | | **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | - | ### Description : This is not a bug report but merely a suggestion for discussion. According to the "Liskov substitution principle" (see the English wikipedia article of that name for references) a method in a subclass should have a stronger (or equivalent) contract that the corresponding method in the superclass. It could make sense to provide a corresponding check within Frama-Cxx, which could be enabled or disabled by an appropriate command-line option. This check would be negative (i.e. unprovable) for the attached program "140.cpp"; however, it would be positive if "==" in line 3 was changed to ">=". So this program can be used as a simple test case for such a check, if and when it is implemented. ## Attachments - [140.cpp](/uploads/1bc224ee781810c444a06c34ee30f3e8/140.cpp)