How to prove a statement containing pointer operations

Question

I am trying to prove a simple statement using the frama-c WP plugin. C code was created from the Targetlink lookup table. My goal is to provide a sufficient number of function annotations so that I can use the resulting contract to prove the properties of the calling program. As a first step, I wrote a statement near the beginning of a function that compares a constant with a value obtained from dereferenced pointers, see the following example.

typedef struct MAP_Tab1DS0I2T3_b_tag { int Nx; const int * x_table; const int * z_table; } MAP_Tab1DS0I2T3_b; int LARA_GearEnaCndn_X[9] = { -1, 0, 1, 2, 3, 4, 5, 6, 8 }; int LARA_GearEnaCndn_Z[9] = { 1, 0, 1, 1, 0, 0, 0, 0, 0 }; MAP_Tab1DS0I2T3_b Sb218_LARA_GearEnaCndn_CUR_map = { 9, (const int *) &(LARA_GearEnaCndn_X[0]), (const int *) &(LARA_GearEnaCndn_Z[0]) }; /*@ requires x == 2; */ int Tab1DS0I2T3_b(const MAP_Tab1DS0I2T3_b * map, int x) { /* SLLocal: Default storage class for local variables | Width: 8 */ int Aux_U8; int Aux_U8_a; int Aux_U8_b; int Aux_U8_c; /* SLLutLocalConst: Default storage class for local variables | Width: 32 */ const int * x_table /* Scaling may differ through function reuse. */; const int * z_table /* Scaling may differ through function reuse. */; x_table = map->x_table; z_table = map->z_table; //@ assert (x < x_table[(int) (map->Nx - 1)]); if (x <= *(x_table)) { /* Saturation. */ return z_table[0]; } if (x >= x_table[(int) (map->Nx - 1)]) { return z_table[(int) (map->Nx - 1)]; } /* Linear search, start low. */ x_table++; while (x > *(x_table++)) { z_table++; } x_table -= 2 /* 2. */; Aux_U8 = *(z_table++); Aux_U8_a = *(z_table); /* Interpolation. */ Aux_U8_b = (int) (((int) x) - ((int) x_table[0])); Aux_U8_c = (int) (((int) x_table[1]) - ((int) x_table[0])); if (Aux_U8 <= Aux_U8_a) { /* Positive slope. */ Aux_U8 += ((int) ((((int) (int) (Aux_U8_a - Aux_U8)) * ((int) Aux_U8_b)) / Aux_U8_c)); } else { /* Negative slope. */ Aux_U8 -= ((int) ((((int) (int) (Aux_U8 - Aux_U8_a)) * ((int) Aux_U8_b)) / Aux_U8_c)); } return Aux_U8; } 

Can someone give me a hint what annotations do I need in order to succeed? From the look at the Coq proof commitment, I see that there are no axioms for operations like addr_of_data or access that I need to rewrite terms. There is also no information about the global variables referenced in the statement.

 1 subgoals ______________________________________(1/1) forall x_0 map_0 : Z, is_sint32 x_0 -> forall m_0 : array data, x_0 = 2 -> forall x_table_0 : Z, x_table_0 = addr_of_data (access m_0 (addr_shift map_0 1)) -> 2 < sint32_of_data (access m_0 (addr_shift x_table_0 (as_sint32 (sint32_of_data (access m_0 (addr_shift map_0 0)) - 1)))) 

BR, Harald

Answer 1

Elements addr_of_data strong>, addr_shift , etc. are automatically indicated on the store_model.v tab of your coq-ide.

In your example, it is not indicated anywhere that the card receives Sb218_LARA_GearEnaCndn_CUR_map as the actual parameter. Without this, the statement may be erroneous.

Now I do not know how to make wp use the explicit values ​​of the global initializers as part of the proof. There are several global invariants in ACSL, but wp doesn't seem to handle them anyway. Therefore, I will use explicit require statements for the required values.

Given the following set of statements in the function header:

 /*@ requires x == 2; requires map->x_table == Sb218_LARA_GearEnaCndn_CUR_map.x_table; requires map->Nx == Sb218_LARA_GearEnaCndn_CUR_map.Nx; requires LARA_GearEnaCndn_X[8] == 8; requires Sb218_LARA_GearEnaCndn_CUR_map.Nx == 9; requires Sb218_LARA_GearEnaCndn_CUR_map.x_table == LARA_GearEnaCndn_X; requires Sb218_LARA_GearEnaCndn_CUR_map.z_table == LARA_GearEnaCndn_Z; */ 

I was able to prove the necessary statement.

The first is yours. The second and third are explicit extensions *map=Sb218_LARA_GearEnaCndn_CUR_map so as not to be confused with address ranges. The rest reflects the values ​​of the initializer.