--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on March 2013 ---
Hello, We are implementing a filter that is used in a flight control software. The filter algorithm is implemented as a iterative process whose next iteration is calculated based on the previous calculated value. In that process, the successive calculations with the Cvo_Xf and Cvo_Fqrp variables imply accumulated values that grow until reaching the maximum value of the double variable. Is there an annotation or a command line option to deal with this type of iterative algorithm? It is noticed that using a single value instead of an interval, the algorithm works well. We ran the following line command and some parts of the log file is shown bellow >> frama-c -val filter.c /usr/share/frama-c/builtin.c -slevel 3840 > log.txt Cvo_Fqrp ??? [-0.441164442315 .. 0.439403377322] Cvo_Xf[0] ??? {0; } [1] ??? [-0.441164442315 .. 0.439403377322] ... Cvo_Fqrp ??? [-1.72477568729 .. 1.72394440298] Cvo_Xf[0] ??? [-0.441164442315 .. 0.439403377322] [1] ??? [-0.968026842207 .. 0.964162618303] ... Cvo_Fqrp ??? [-3.8465662583 .. 3.84574818041] Cvo_Xf[0] ??? [-0.968026842207 .. 0.964162618303] [1] ??? [-1.75390847835 .. 1.7481604756] ... Cvo_Fqrp ??? [-1.79769313486e+308 .. 1.79769313486e+308] Cvo_Xf[0..1] ??? [-1.79769313486e+308 .. 1.79769313486e+308] Xfaux ??? [-1.79769313486e+308 .. 1.79769313486e+308] Best regards, Nanci, Rovedy and Luciana double Cvo_Fqrp; double Cvo_Xf [2]; double a; double F_Kf = 6.306410E-1; double F_A1 = -1.194254E+0; double F_A2 = 3.565610E-1; double F_B1 = -1.722219E+0; double F_B2 = 9.795862E-1; void main () { double msiARF; int i; Cvo_Xf[0] = 0.0; Cvo_Xf[1] = 0.0; msiARF = Frama_C_float_interval(-0.699549255939, 0.696756755939); for ( i =0; i<3840; i++) { a=msiARF; filter(); Frama_C_dump_each(); } } void filter () { double Xfaux; Cvo_Fqrp = a; Xfaux = F_Kf * Cvo_Fqrp - F_A2 * Cvo_Xf[0] - F_A1 * Cvo_Xf[1]; Cvo_Fqrp = Xfaux + F_B2 * Cvo_Xf[0] + F_B1 * Cvo_Xf[1]; Cvo_Xf[0] = Cvo_Xf[1]; Cvo_Xf[1] = Xfaux; Frama_C_show_each_Cvo_Fqrp_I_(Cvo_Fqrp); } -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130315/534891d5/attachment.html>