--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on June 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Query about Frama-C specifications



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>