--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on May 2013 ---
[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