Frama-c, non-deterministic float values

Question

As example I use the following function:

float nondet_float(){
  float x;
  return x;
}

int main(){
  float x = nondet_float();
  if(isnan(x)){
    some_error();
  }
}

I wonder how I have to use frama-c, to simulate non-deterministic floats.

Want I want is, that the variable x, is considered to be any possible float value, including -inf, +inf and NaN.

I'd like to get the result that some_error() is reachable, if x is NaN.

So my question is:

how do I simulate non-deterministic floats? how do I test for reachability of certain function calls?

Answer 1

Frama-C is a collection of plugin, with different level of support for infinite/NaN floating-point values. I believe WP supports NaN and infinites; but this probably depend on the numeric model you choose (option -wp-model).

For the abstract interpretation plugin (EVA, formerly Value), NaN and infinites are not supported for the moment. The analyzer supposes (and proves) that all floating-point values are finite. Support for non-finite ones will be added in Frama-C Sulfur.

Also, your nondet_float function is invalid in any case. Returning uninitialized values is forbidden by the C standard, and this function will be flagged as incorrect by e.g. EVA. Instead, you should use a function without a body, with the clause assigns \result \from \nothing as its specification.