Frama-C should return a non-null return value when a goal could not be validated
ID0000987: **This issue was created automatically from Mantis Issue 987. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0000987 | Frama-C | Kernel | public | 2011-10-17 | 2012-02-15 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | sylvain nahas | **Assigned To** | signoles | **Resolution** | no change required | | **Priority** | normal | **Severity** | feature | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - | ### Description : Feature description: Currently Frama-C returns a value of 0 to the OS whatever are the status of the proof obligations. It should provide a command line switch that makes him return a non-null value in this case. The default behavior would stay the same. Use-Case: QA purposes. The need arise when automatizing source code validation with Makefiles. Makefile will stop execution when a building command returns a value different of 0, but this does not function with Frama-C, even if one may wish to stop the build when the source is not completely validated. In the last case a completed build run means 100% validated code with respect to annotations. This would be useful as well when writing hooks script on VCS servers (think subversion). Note: the option may provide several levels. ## Attachments - [werror.tar.gz](/uploads/6dcc54de1a5aff3fa68a89dd10c7b8fe/werror.tar.gz) - [werror-2.tar.gz](/uploads/aedb35ba264bd980d43396a67ba0ceca/werror-2.tar.gz)
issue