--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on June 2015 ---
We are experimenting with Frama-C function contracts in our programs. We took a sample program to write the annotations and prove the correctness of the program using WP plugin. with AltErgo theorem prover. However we are unable to prove the program correctness with the specifications laid on it using ACSL. Hence we need help from FRAMA C community to understand what exactly is wrong with the specifications. Below is the description of the intended program: We have an integer array of 3 elements. If any of its two elements are greater than a value "v" then the result of the function should be 1 else the result should be zero. With this email, we are attaching the code with the annotations. After running the code provided with annotations, post conditions mentioned in the function contract is not proven to be satisfed by the theorem prover. Please look into the problem and suggest. Thanks all Sowmya -------------- next part -------------- A non-text attachment was scrubbed... Name: 3sample.odt Type: application/vnd.oasis.opendocument.text Size: 26176 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150602/35609a4e/attachment-0001.odt>