--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on August 2013 ---
On 08/22/2013 07:02 PM, Rovedy Aparecida Busquim e Silva wrote: > Hi, > > We are sending the working version of the code without the if statements. > > According to tutorial, we have followed the below sequence: > - identify variables modified in the loop: > - use loop assigns clause to list variables that (might) have been > assigned so far after iterations > - define their possible value intervals (relationships) after iterations > > In our case, we identified the variables j and soma that were modified > in the loop. > > Because of that, we tried to specify the variable soma. I think the question you should ask yourself is what would you like to specify about soma first, in English. It is seems natural to specify that at each loop iteration, soma is the sum of elements of array acel for index between 0 to j-1. I recommend to look at the example tests/c/sum_array.c of the Why 2.33 distrib. Here it is as attachment > float acel[3], soma; > > void test() > { > int j; > > acel[0] = 5.0; > acel[1] = 5.0; > acel[2] = 5.0; > > soma = 0.0; There is a big difference in this version: values acel[0..] are initialized. It is then clear true that all acel[k], for 0<=k<3, are >= 0 The formula in the loop inv is thus true, -------------- section suivante -------------- Une pi?ce jointe autre que texte a ?t? nettoy?e... Nom: sum_array.c Type: text/x-csrc Taille: 1492 octets Desc: non disponible URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130822/edaf65dc/attachment.c>