How to prove integers are finite in Frama-C

I have a little snippet of c that looks like this:

double sum(double a, double b) {
return a+b; }

When I run this with eva-wp, I get the error:

non-finite double value. assert \is_finite(\add_double(a, b));

But when I add :

requires \is_finite(\add_double(a, b));

then it gets status unknown.

I feel like I'm making a very simple mistake, but I don't know what it is!

Solution

If we consider file.c:

/*@ requires \is_finite(\add_double(a,b)); */
double sum(double a, double b) {
  return a+b;
}

and launch Eva with frama-c -eva -main sum file.c, we indeed have an Unknown status, and the alarm is still there. In fact, these are two separate issues.

First, when there is a requires clause in the main entry point, Eva tries to evaluate it against the generic initial state that it computes anyway, in which double values can be any finite double (or even infinite or NaN, depending on the value of the kernel option -warn-special-float). In this generic state, the requires does not hold, hence the Unknown status.

Second, Eva is not able to take advantage of the requires clause to reduce this initial state to an abstract state in which the property holds: this would require maintaining some kind of relation between a and b, which is not in the scope of the abstract domains currently implemented within Eva. Hence, the analysis is done with exactly the same abstract state as without the requires, and leads to the same alarm.

In order to validate the requires (and make the alarm disappear), you can use a wrapper function, that will build a more appropriate initial state and call the function under analysis, as in e.g.

#include <float.h>
#include "__fc_builtin.h"
/*@ requires \is_finite(\add_double(a,b)); */
double sum(double a, double b) {
  return a+b;
}

void wrapper() {
  double a = Frama_C_double_interval(-DBL_MAX/2, DBL_MAX/2);
  double b = Frama_C_double_interval(-DBL_MAX/2, DBL_MAX/2);
  double res = sum(a,b);
}

Frama_C_double_interval, declared in __fc_builtin.h in $(frama-c -print-share-path)/libc together with similar functions for other scalar types, returns a random double between the bounds given as argument. Thus, from the point of view of Eva, the result is in the corresponding interval. By launching frama-c -eva -main wrapper file.c, we don't have any alarm (and the requires is valid). More generally, such wrappers are usually the easiest way to build an initial state for conducting an analysis with Eva.