Timeout while proving the WP using Alt-ergo on Frama C

Question

I was trying to verify the correctness of the below program using Frama-c.I am new user to frama-C.

PROBLEM:

Input basic salary of an employee and calculate its Gross salary according to following:

Basic Salary <= 10000 : HRA = 20%, DA = 80%

Basic Salary <= 20000 : HRA = 25%, DA = 90%

Basic Salary > 20000 : HRA = 30%, DA = 95%

#include <limits.h>

 /*@requires sal >= 0 && sal <= INT_MAX/2;
   ensures \result > sal && \result <= INT_MAX[enter image description here][1];

   behavior sal1:
   assumes sal <= 10000;
   ensures \result == sal+(sal*0.2*0.8);
   behavior sal2:
   assumes sal <= 20000;
   ensures \result == sal+(sal*0.25*0.9);
   behavior sal3:
   assumes sal >20000;
   ensures \result == sal+(sal*0.3*0.95);
   complete behaviors sal1,sal2,sal3;
  */


double salary(double sal){
    if(sal<=10000){return (sal+(sal*0.2*0.8));}
    else if(sal<=20000){return (sal+(sal*0.25*0.9));}
    else{return (sal+(sal*0.3*0.95));}
}

what mistake am i making here? should the precondition be more precise.

console message:

[wp] [Alt-Ergo 2.3.3] Goal typed_salary_ensures : Timeout (Qed:57ms) (10s) 
(cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_salary_assert_rte_is_nan_or_infinite_3 : 
Timeout (Qed:20ms) (10s) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_salary_assert_rte_is_nan_or_infinite_6 : 
Timeout (Qed:2ms) (10s) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_salary_assert_rte_is_nan_or_infinite_5 : 
Timeout (Qed:2ms) (10s) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_salary_assert_rte_is_nan_or_infinite_4 : 
Timeout (Qed:17ms) (10s) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_salary_assert_rte_is_nan_or_infinite_7 : 
Timeout (Qed:15ms) (10s) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_salary_sal1_ensures : Timeout (Qed:33ms) 
(10s) (cached)
 [wp] [Alt-Ergo 2.3.3] Goal typed_salary_assert_rte_is_nan_or_infinite_9 : 
 Timeout (Qed:2ms) (10s) (cached)
 [wp] [Alt-Ergo 2.3.3] Goal typed_salary_assert_rte_is_nan_or_infinite_8 : 
 Timeout (Qed:4ms) (10s) (cached)
 [wp] [Alt-Ergo 2.3.3] Goal typed_salary_sal2_ensures : Timeout (Qed:42ms) 
 (10s) (cached)
 [wp] [Alt-Ergo 2.3.3] Goal typed_salary_sal3_ensures : Timeout (Qed:35ms) 
 (10s) (cached)

Answer 1

Automated theorem provers behave generally quite poorly when confronted to floating-point computation (see e.g. this report). If you really, really need them, you may want to install Gappa, which is specialized for that, or hope that using CVC4, Z3 and Alt-Ergo (as opposed to just Alt-Ergo) will allow you to have at least one prover able to discharge each proof obligation. But I'd advise to stick to integer arithmetic, e.g. by using cents as unit in order to only manipulate integers when computing percentages (EDIT: since your multiplying percentages, this would mean working with 1/10000 units, but it still shouldn't be a problem). In fact, if you insist on doubles, the requirements to have values less than INT_MAX does not make much sense.

In the same vein, if you use an integer type, it's probably easier to go for unsigned, which will automatically fulfill the requirement of having a non-negative salary.

Finally, your specification is ambiguous: for any salary less than 10000, you have two distinct formulas to compute the result. the assumes clause of behavior sal2 should probably read: assumes 10000 < sal <= 20000;