--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on May 2013 ---
Hello, 2013/5/16 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>: > We would like to ask you a suggestion about an algorithm in our case study. > Our case study is complex and it is composed of several functions. > Almost all of them were correctly verified by Frama-c Value Analysis plugin > and gave the expected results, except one. > > To exemplify the situation, we simplified the program to send to you. > We calculate some variables (test1 and test2) that must be between a range > (-BETA_SAT and BETA_SAT). > The function Limit() checks the bounds and verify which variable has the > larger absolute value (test2 in our example), > this variable receives the limit value (BETA_SAT) with the correct signal. > The other variable (test1 in our example) receives the proportional > correction. > BETA_SAT is not defined in your code. I guess that it is also an interval? If this is the case and you have BETA_SAT=Frama_C_interval(0.,15.) for instance, you indeed have an issue, because of the lack of relation between max and BETA_SAT. Somehow, you have to force value to recognize the fact that when BETA_SAT's magnitude is very small, then so is max, so that the division is safe. This can be done by splitting the interval for BETA_SAT, using a disjunction of the form /*@ assert 0<= BETA_SAT < 0x1p-1074 || 0x1p-1074 <= BETA_SAT < 0x1p-1073 || ... || 0.5 <= BETA_SAT <1. || 1<= BETA_SAT; */ and an appropriate slevel. Of course, said disjunction would be generated by a script rather than written by hand. The number of subdivisions may probably be adapted depending on precision needs and run time of the analysis. Best regards, -- E tutto per oggi, a la prossima volta Virgile