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