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] [Value Analysis] Interval Division

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