Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Query about Frama-C specifications
  • From: mitra2270 at gmail.com (sowmya mitra Attaluri)
  • Date: Tue, 2 Jun 2015 11:55:54 +0530
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>