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] Problem with ACSL annotations

  • Subject: [Frama-c-discuss] Problem with ACSL annotations
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Wed, 19 Dec 2012 12:00:37 +0000
Hello Initisar,

you source code looks difficult to read in my mail client (there are a lot of question) marks.
I guess your function is related to find the largest value in an array?
If so, then I can recommend a look on on Chapter 4 of ourACSL tutorial

http://www.fokus.fraunhofer.de/de/quest/_download_quest/_projekte/acsl_by_example.pdf

Regards

Jens


/*@ requires \valid_range(queue,0,14);
??? assigns \nothing;
??? ensures \exists int e; 0<=e && (\forall int i; 0<=i<15 && e > queue[i]) && ( (e >= 5) || (e >= 10) ) ==> \result == 0;
??? ensures \exists int e; 0<=e && (\forall int i; 0<=i<15 && e > queue[i]) && ( (e < 5) && (e < 10) ) ==> \result == e;
??? 
???? 
*/
int find_array_max(int queue[15]){
?int i, largest;

? largest = 0;
/*@ loop variant 15 - i;
??? loop invariant 0 <= i <= 15;
??? 
*/
? for (i = 0; i < 15; i++) {
??? if (queue[i] > largest)
????? largest = queue[i];
? }
? if ( (largest >= 5) || (largest >=10) ) {
??? 
??? ? return 0;
? }
?? return largest;

}

--

Please note my new email address.

Dr.-Ing. Jens Gerlach 
Quality for Embedded Systems (QUEST)
Phone +49 (0)30 6392 1841, jens.gerlach at fokus.fraunhofer.de
Fraunhofer Institute for Open Communication Systems
Fraunhofer FOKUS, Kekulestrasse 7, D 12489 Berlin, Germany