How does one prove simple equalities of non-deterministic values in Frama-C + EVA?

Question

I'm a bit confused by the behavior of Frama-C version 18.0 (Argon).

Given the following program:

#include <assert.h>
#include <limits.h>


/*@ requires order: min <= max;
    assigns \result \from min, max;
    ensures result_bounded: min <= \result <= max ;
 */
extern int Frama_C_interval(int min, int max);


int main() {

  int i,j;

  i = Frama_C_interval(INT_MIN, INT_MAX);

  j = i;

  assert(j == i);

  return 0;
}

I'd expect the assertion to be proven quite easily with any of the abstract domains which track equality. However, invoking

frama-c -eva -eva-equality-domain -eva-polka-equalities foo.c

Gives:

[eva] Warning: The Apron domains binding is experimental.
[kernel] Parsing stupid_test.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization

[eva] using specification for function Frama_C_interval
[eva] using specification for function __FC_assert
[eva:alarm] foo.c:20: Warning: 
  function __FC_assert: precondition 'nonnull_c' got status unknown.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  i ∈ [--..--]
  j ∈ [--..--]
  __retres ∈ {0}

Am I missing something?

Answer 1

Interesting. Your example is not handled by -eva -eva-equality-domain, which was written with other purposes in mind. As such, the special case for x == y when x and y are known to be equal has not been written. This would be fairly easy to add.

(Given the name of the domain, this might come across as surprising. The equality domain is more geared towards enabling more backwards propagation when we have uninteresting aliases, for example temporaries added by the kernel.)

Regarding the domains coming from Apron, this is more surprising. I modified your example as such:

  j = i;

  int b = j - i;
  int c = j == i;
  Frama_C_dump_each_domain();

Running frama-c -eva -eva-polka-equalities foo.c -value-msg-key d-apron gives the following result:

[eva] c/eq.c:23: 
  Frama_C_dump_each_domain:
  # Cvalue domain:
  i ∈ [--..--]
  j ∈ [--..--]
  b ∈ {0}
  c ∈ {0; 1}
  __retres ∈ UNINITIALIZED
  # Polka linear equalities domain:
  [|-i_44+j_45=0; b_46=0|]

As you can see, Apron has inferred the relation between i and j (the suffix is the line number), simplified b to 0, but has not simplified c to 1. This is surprising to me, but explains the imprecision you observed. It does not work either with the octagons domain.

I'm not that familiar with abstract transformers on relational domains so this may be expected, but this is certainly puzzling. The code to handle relational operators exist in Frama-C/Eva/Apron, but is partly home-written (it is not just a simple call to an Apron primitive). In particular, it calls the operator for subtraction, and analyzes the equality of the result with 0. It is hard to see why b would be precise but not c.

Answer 2

Update: on more recent Frama-C versions (I tried with Frama-C 25.0, but it will surely work on some older versions as well), the octagon domain is able to handle that specific case: -eva -eva-domains octagon is sufficient, in your specific code, to avoid the alarm.

Also note that the octagon domain can be indirectly enabled with option -eva-precision 5 (or higher).