--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on December 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with ACSL annotations



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