How to specify variable bounds in a clean way?

/*@
    requires 0 <= lb < N_LOG_BLOCKS &&  0 <= lp < N_PAGE ;
    requires  (  1 <= h_clean_counter + l_clean_counter <= N_PHY_BLOCKS );
    requires 0 <= h_act_block_index_p < N_PHY_BLOCKS &&   0 <= h_act_page_p < N_PAGE;
    requires 0 <= l_act_block_index_p < N_PHY_BLOCKS &&   0 <= l_act_page_p < N_PAGE;
    requires 0 <= l_to_p[lb][lp] < N_PHY_BLOCKS * N_PAGE || l_to_p[lb][lp] == -1;
    requires -2147483648 <= d <= 2147283647 ;
    requires 0 <=  chance_index_p < LRU_SIZE;
    requires 0 <= index_2_physical[h_act_block_index_p] < N_PHY_BLOCKS ;
    requires \forall integer i; 0 <= i < N_PHY_BLOCKS ==> 0 <= index_2_physical[i] < N_PHY_BLOCKS;

    requires 0 <= l_array_counter < N_PHY_BLOCKS/2;
    requires l_clean_counter == low_array_counter;
    requires h_clean_counter == high_array_counter;
...
*/

My code has tons of variables with some intended bound. As a result, I need to put all these bound constraints in all "requires" and "ensures" regions of all functions. I wonder whether there is a smarter way for me to specify the variable bound, preferably in a global manner.

Solution

If these bounds are indeed the same for all functions and you have global variables or the formals are consistently named across all functions, I'd say that this is something MetAcsl can do for you, with something like (for your first requires)

/*@ meta \prop,
  \name(lb_bounds),
  \context(\precond),
  \targets(\ALL),
  0 <= lb < N_LOG_BLOCKS;
*/

[NB: I haven't tried to type-check it, it may contain typos]

Basically, this tells MetAcsl to insert a pre-condition (because of the \precond context) to \ALL functions saying 0<= lb < N_LOG_BLOCKS. You can find more information about the annotations that can be generated by MetAcsl on its gitlab repository.