Higher-precision options (`slevel` and `partition-history`) in Eva unexpectedly increases alarm count

Analyzing a simplified parser_full.c (derived from OSCS repository, removed unrelated functions and ACSL annotations for simplicity) shows counterintuitive behavior:

Core Questions:

1. Why would higher-precision options increase alarms in this case?
2. How does nested while-loop in print_diff_child_age(p_id) (called by run() at line 60) interact with these parameters (specifically, -eva-slevel and -eva-partition-history)?
3. Are these additional alarms false positives? (Does Frama-C/Eva still maintain soundness in this case?)

/* A modified version of parser_full.c from Open source case studies. */

#include <__fc_builtin.h>
#include <stdint.h>
#include <stdio.h>

#define MAX_CHILDREN_LEN 10
#define MAX_BUF_SIZE 100
#define MAX_PERSON_NUMBER 50

struct person {
  uint8_t age;
  uint8_t children_len;
  uint8_t children[MAX_CHILDREN_LEN];
};

struct person p[MAX_PERSON_NUMBER];

int parse(uint8_t *buf, uint16_t *offset, uint16_t len, uint8_t p_id){
  if(! (sizeof(uint8_t) <= len - *offset) ) return -1;
  p[p_id].age = (uint8_t) buf[*offset];
  *offset += sizeof(uint8_t);

  if(! (sizeof(uint8_t) <= len - *offset)) return -1;
  p[p_id].children_len = (uint8_t) buf[*offset];
  *offset += sizeof(uint8_t);

  if(! (p[p_id].children_len < MAX_CHILDREN_LEN)) return -1;

  for(uint8_t child_id = 0; child_id < p[p_id].children_len; child_id++){
    if(! (sizeof(uint8_t) <= len - *offset)) return -1;
    p[p_id].children[child_id] = (uint8_t) buf[*offset];

    if(! (p[p_id].children[child_id] < p_id) ) return -1;
    *offset += sizeof(uint8_t);
  };

  return 0;
};

void print_diff_child_age(uint8_t p_id){
  printf("%i(%i) :", p_id,p[p_id].age);
  for(uint8_t i = 0; i < p[p_id].children_len; i++){
    printf(" %i",p[p_id].age - p[p[p_id].children[i]].age);
  }

  printf("\n");
}

uint64_t run(uint8_t *buf, uint16_t len){
  uint16_t offset = 0;
  uint8_t p_nb;

  for(p_nb = 0; p_nb < MAX_PERSON_NUMBER; p_nb++){
    int r = parse(buf, &offset, len, p_nb);
    if(r) break;
  }

  for(uint8_t p_id = 0; p_id < p_nb; p_id++){
    print_diff_child_age(p_id);
  }

  return 0;
}

int main(){
  uint8_t buf[MAX_BUF_SIZE];
  uint16_t len = MAX_BUF_SIZE;
  Frama_C_make_unknown((char*)buf,MAX_BUF_SIZE);

  run(buf,len);

  return 0;
};

The simplified version of low-precision-0-alarms.log:

[kernel] Parsing parser_full.c (with preprocessing)
[eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
  option -eva-min-loop-unroll set to 0 (default value).
  option -eva-auto-loop-unroll set to 128.
  option -eva-widening-delay set to 3 (default value).
  option -eva-partition-history set to 0 (default value).
  option -eva-slevel already set to 2000 (not modified).
  option -eva-ilevel set to 48.
  option -eva-plevel set to 150.
  option -eva-subdivide-non-linear set to 100.
  option -eva-remove-redundant-alarms set to true (default value).
  option -eva-domains set to 'cvalue,equality,gauges,octagon,symbolic-locations'.
  option -eva-split-return set to 'auto'.
  option -eva-equality-through-calls set to 'formals' (default value).
  option -eva-octagon-through-calls set to false (default value).

...

[eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  4 functions analyzed (out of 4): 100% coverage.
  In these functions, 71 statements reached (out of 71): 100% coverage.
  ----------------------------------------------------------------------------
  No errors or warnings raised during the analysis.
  ----------------------------------------------------------------------------
  0 alarms generated by the analysis.
  ----------------------------------------------------------------------------
  Evaluation of the logical properties reached by the analysis:
    Assertions        0 valid     0 unknown     0 invalid      0 total
    Preconditions     4 valid     0 unknown     0 invalid      4 total
  100% of the logical properties reached have been proven.
  ----------------------------------------------------------------------------

The simplified version of high-precision-2-alarms.log:

[kernel] Parsing parser_full.c (with preprocessing)
[eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
  option -eva-min-loop-unroll set to 0 (default value).
  option -eva-auto-loop-unroll set to 128.
  option -eva-widening-delay set to 3 (default value).
  option -eva-partition-history already set to 2 (not modified).
  option -eva-slevel already set to 5000 (not modified).
  option -eva-ilevel set to 48.
  option -eva-plevel set to 150.
  option -eva-subdivide-non-linear set to 100.
  option -eva-remove-redundant-alarms set to true (default value).
  option -eva-domains set to 'cvalue,equality,gauges,octagon,symbolic-locations'.
  option -eva-split-return set to 'auto'.
  option -eva-equality-through-calls set to 'formals' (default value).
  option -eva-octagon-through-calls set to false (default value).

...

[eva:alarm] parser_full.c:44: Warning: 
  accessing out of bounds index. assert p[p_id].children[i] < 50;
[eva:alarm] parser_full.c:44: Warning: 
  accessing out of bounds index. assert i < 10;

...

[eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  4 functions analyzed (out of 4): 100% coverage.
  In these functions, 71 statements reached (out of 71): 100% coverage.
  ----------------------------------------------------------------------------
  No errors or warnings raised during the analysis.
  ----------------------------------------------------------------------------
  2 alarms generated by the analysis:
       2 accesses out of bounds index
  ----------------------------------------------------------------------------
  Evaluation of the logical properties reached by the analysis:
    Assertions        0 valid     0 unknown     0 invalid      0 total
    Preconditions     4 valid     0 unknown     0 invalid      4 total
  100% of the logical properties reached have been proven.
  ----------------------------------------------------------------------------

The bulk of the issue is hidden in this sentence of section 6.4.1 of the Eva manual:

Also, -eva-slevel does not allow fine grained control as loop unrolling annotations, it is context-dependent (e.g. for nested loops), unstable (minor changes in control flow may affect the usage of slevel) and hard to estimate in presence of complex control flows.

In particular, when you use -eva-partition-history 2, Eva spends a lot of slevel discriminating against the various possible failure in parse, while we're only interested in two outcomes: it returns 0 and the values in the .children array are correct, or it returns -1. Moving from 3000 to 5000 does not compensate this increased number of cases, and Eva ends having not enough slevel when entering the printing loop.

Splits and loop unrolling are in fact easier to manage consistently. A possibility with your example is to add the annotation //@ split p_nb; after the first loop in run, to ensure you keep the relation between p_nb and the number of elements of p that have been properly initialized, and use the following command line:

frama-c -eva -eva -eva-split-return-function parse:0 -eva-slevel 100 parser_full.c

to obtain an appropriate precision level in parse and print_diff_child_age. It also takes much less time to compute that -eva-precision 5.

NB: problems like this are not easy to visualize in the graphical user interface, which shows the results after the analysis has completed: all separated states are joined, there's only a distinction per call stack. In order to visualize separated states, you have to resort to Frama_C_show_each() calls, as explained in Section 9.3 of the Eva manual.