Shall we write "assert" after each function call when a sequence of functions are called?

Question

Let me start my question by this example:

void A (void)
{
  B();
  C();
  D();
  E();
  ... // function calls go on.

  return;
}

Now let's add ACSL annotations to the code:

/*@
   ensures PostConditionOfB();
   ensures PostConditionOfC();
   ensures PostConditionOfD();
   ensures PostConditionOfE();
   ... // ensuring the predicates of the remaining functions goes on.
*/
void A (void)
{
  B();
  C();
  D();
  E();
  ... // function calls go on.

  return;
}

I asked Frama-C to check the code by executing "frama-c-gui -wp file.c". The contract marked valid when the functions B, C and D were called in the function A. By Adding the call of function E and probably more other functions, the contract was marked invalid. We came up with the idea of adding "assert" right after each function call to give Frama-C a clue which postconditions are assumed to be satisfied. By this approach, the contract was marked valid. Check out the code:

/*@
   ensures PostConditionOfB();
   ensures PostConditionOfC();
   ensures PostConditionOfD();
   ensures PostConditionOfE();
   ... // ensuring the predicates of the remaining functions goes on.
*/
void A (void)
{
  B();
  //@ assert PostConditionOfB();
  C();
  //@ assert PostConditionOfB();
  //@ assert PostConditionOfC();
  D();
  //@ assert PostConditionOfB();
  //@ assert PostConditionOfC();
  //@ assert PostConditionOfD();
  E();
  //@ assert PostConditionOfB();
  //@ assert PostConditionOfC();
  //@ assert PostConditionOfD();
  //@ assert PostConditionOfE();
  ... // function calls go on.

  return;
}

Here's the question: is there a better approach for checking the contract of a function that includes several function calls rather than adding "assert" right after each function call?

Updated Code:

The file.h looks as follows:

#define SIZE_FIRST 100
#define SIZE_SECOND 30
#define SIZE_THIRD 30

typedef struct
{
int  Field_5;
int  Field_6;
} Struct_C;

typedef struct
{
int Field_1;
int Field_2;
int Field_3;
int Field_4;
Struct_C At_1 [ SIZE_SECOND ];
Struct_C At_2 [ SIZE_THIRD ];
Struct_C At_3 [ SIZE_THIRD ];
} Struct_B;

typedef struct
{
 Struct_B At [ SIZE_FIRST ];
 int Count;
} Struct_A;

/*@ predicate
  Reset_Basics (Struct_B * Stct_B) =
   (Stct_B->Field_1 == 0) &&
   (Stct_B->Field_2 == 0) &&
   (Stct_B->Field_3 == 0) &&
   (Stct_B->Field_4 == 0);
*/

/*@ predicate 
  Reset_At_1 (Struct_B * Stct_B, integer First, integer Last) =
    \forall integer Index; First <= Index < Last ==>
                (Stct_B->At_1 [ Index ].Field_5 == 0) &&
                (Stct_B->At_1 [ Index ].Field_6 == 0);
*/


/*@ predicate 
  Reset_At_2 (Struct_B * Stct_B, integer First, integer Last) =
    \forall integer Index; First <= Index < Last ==>
                (Stct_B->At_2 [ Index ].Field_5 == 0) &&
                (Stct_B->At_2 [ Index ].Field_6 == 0);
*/

/*@ predicate 
  Reset_At_3 (Struct_B * Stct_B, integer First, integer Last) =
    \forall integer Index; First <= Index < Last ==>
                (Stct_B->At_3 [ Index ].Field_5 == 0) &&
                (Stct_B->At_3 [ Index ].Field_6 == 0);
*/

The file.c looks as follows:

#include "file.h"

void Initialize (Struct_A * const Stct_A);
void Reset (Struct_B * const Stct_B);
void Reset_Basics (Struct_B * const Stct_B);
void Reset_At_1 (Struct_B * const Stct_B);
void Reset_At_2 (Struct_B * const Stct_B);
void Reset_At_3 (Struct_B * const Stct_B);

/*@ 
   assigns Stct_A->At [ 0..(SIZE_FIRST - 1) ];
   assigns Stct_A->Count;
*/
void Initialize (Struct_A * const Stct_A)
{

/*@
 loop invariant 0 <= Index <= SIZE_FIRST;

 loop invariant \forall integer Stct_B_Index; (0 <= Stct_B_Index < 
      Index) ==> Reset_Basics(&(Stct_A->At [ Stct_B_Index ]));

 loop invariant \forall integer Stct_B_Index; (0 <= Stct_B_Index < 
      Index) ==> Reset_At_1(&(Stct_A->At [ Stct_B_Index ]), 0,   
      SIZE_SECOND);

 loop invariant \forall integer Stct_B_Index; (0 <= Stct_B_Index < 
      Index) ==> Reset_At_2(&(Stct_A->At [ Stct_B_Index ]), 0, 
      SIZE_THIRD);

 loop invariant \forall integer Stct_B_Index; (0 <= Stct_B_Index < 
      Index) ==> Reset_At_3(&(Stct_A->At [ Stct_B_Index ]), 0,
      SIZE_THIRD);

 loop assigns Index, Stct_A->At [ 0..(SIZE_FIRST - 1) ];

 loop variant SIZE_FIRST - Index;
*/
 for (int Index = 0; Index < SIZE_FIRST; ++(Index))
  {
   Reset(&(Stct_A->At [ Index ]));
  } 

  Stct_A->Count = 0;

 return;
 }

/*@ 
  assigns * Stct_B;
  ensures Reset_Basics(Stct_B);
*/
void Reset_Basics (Struct_B * const Stct_B) 
{

  Stct_B->Field_1 = 0;
  Stct_B->Field_2 = 0;
  Stct_B->Field_3 = 0;
  Stct_B->Field_4 = 0;

  return; 
}

/*@
  assigns Stct_B->At_1 [ 0..(SIZE_SECOND - 1) ];
  ensures Reset_At_1(Stct_B, 0, SIZE_SECOND);
*/
void Reset_At_1 (Struct_B * const Stct_B)
{
 /*@
 loop invariant 0 <= Index <= SIZE_SECOND;

 loop invariant Reset_At_1(Stct_B, 0, Index);

 loop assigns Index, Stct_B->At_1 [ 0..(SIZE_SECOND - 1) ];

 loop variant SIZE_SECOND - Index;
*/
  for (int Index = 0; Index < SIZE_SECOND; ++(Index))
  {
    Stct_B->At_1 [ Index ].Field_5 = 0;
    Stct_B->At_1 [ Index ].Field_6 = 0;
  }

  return;
 }

/*@ 
  assigns Stct_B->At_2 [0..(SIZE_THIRD - 1)];
  ensures Reset_At_2(Stct_B, 0, SIZE_THIRD);
*/
void Reset_At_2 (Struct_B * Stct_B)
{

 /*@ 
   loop invariant 0 <= Index <= SIZE_THIRD;

   loop invariant Reset_At_2(Stct_B, 0, Index);

   loop assigns Index, Stct_B->At_2 [0..(SIZE_THIRD - 1)];

   loop variant SIZE_THIRD - Index; 
 */ 
  for (int Index = 0; Index < SIZE_THIRD; ++(Index))
   {
     Stct_B->At_2 [ Index ].Field_5 = 0;
     Stct_B->At_2 [ Index ].Field_6 = 0;
   }  

    return;
 }


/*@ 
   assigns Stct_B->At_3 [0..(SIZE_THIRD - 1)];
   ensures Reset_At_3(Stct_B, 0, SIZE_THIRD);
*/
void Reset_At_3 (Struct_B * Stct_B)
{

  /*@ 
   loop invariant 0 <= Index <= SIZE_THIRD;

   loop invariant Reset_At_3(Stct_B, 0, Index);

   loop assigns Index, Stct_B->At_3 [0..(SIZE_THIRD - 1)];

   loop variant SIZE_THIRD - Index; 
   */ 
  for (int Index = 0; Index < SIZE_THIRD; ++(Index))
   {
     Stct_B->At_3 [ Index ].Field_5 = 0;
     Stct_B->At_3 [ Index ].Field_6 = 0;
   }  

  return;
 }

/*@ 
  assigns * Stct_B;
  ensures Reset_Basics(Stct_B);
  ensures Reset_At_1(Stct_B, 0, SIZE_SECOND);
  ensures Reset_At_2(Stct_B, 0, SIZE_THIRD);
  ensures Reset_At_3(Stct_B, 0, SIZE_THIRD);
*/

void Reset (Struct_B * const Stct_B)
{
   Reset_Basics(Stct_B);
   Reset_At_1(Stct_B);
   Reset_At_2(Stct_B);
   Reset_At_3(Stct_B);

  return;
}

It seems to me that there's no guarantee that the post-condition of B still applies after C has been called. C may have been designed to change things so that it will not be true. Rinse and repeat. Having said that, I know nothing of Frama-C and what its assertions mean. I'm mildly intrigued that there are no assertions of pre-conditions, but 'mild' is the operative term and probably only goes to emphasize my lack of any detailed knowledge. — Jonathan Leffler, May 08 '17 at 05:44
How is the contract marked when only the postconditions of the immediatly preceding function calls are asserted? — Yunnosch, May 08 '17 at 06:51
Frama-c checks only for satisfiability of preconditions of a function that is called. It assumes that the postconditions of the function is satisfied without caring about the implementation of the function. Now, I would expect that the assertions of the above code are redundant, but surprisingly the contract of the function A gets invalid without the assertions. — Rocolife, May 08 '17 at 14:31
Again, please post a [minimal, complete and verifiable example](https://stackoverflow.com/help/mcve). In particular, since you have issues with contracts of functions called by `A`, providing their declarations **and their contract** is not an option in such question. Anyways, as hinted at by @jonathan-leffler, the most likely source of the problem is that said contracts lack an `assigns` clause, so that WP has no way of knowing which parts of the global state are changed by functions `C`, `D`, .... Hence, it is not possible to know whether `PostConditionOfB` holds after the call to `C`. — Virgile, May 09 '17 at 06:36
Sorry for the delay. Please take a look at the updated code. In the future I will explain a problem with a clear example that is verifiable. — Rocolife, May 12 '17 at 12:24
First, It seems that the version of Frama-C influences on the results. For example, by using the version Magnesium I didn't need to add any assertion in the code. By the version Neon I had to add assertions as represented in the previous code. Second, after the execution of the updated code by typing "frama-c -wp file.c" I got "timeout" warning. Even by adding the timeout by the command "-wp-timeout" the warning still remained. — Rocolife, May 12 '17 at 12:33
The function Reset() in the updated code is the function that I meant by the function A() in the previous code. — Rocolife, May 12 '17 at 12:42
With Frama-C Silicon, increasing the timeout to 20 seconds is sufficient (on my machine at least) to have everything proved. The issue is likely that alt-ergo has to discover that `Reset_At_3`, `Reset_At_2` and `Reset_At_1` all operate on separate parts of `Stct_B`. — Virgile, May 15 '17 at 07:36
Many thanks. I'll try with Silicon. I think I should install Silicon from source distribution, is that right? Because I installed Frama-c through Opam on Ubuntu and it installed the version Magnesium automatically. Is there a way to upgrade from Magnesium to Silicon? — Rocolife, May 16 '17 at 01:27

Shall we write "assert" after each function call when a sequence of functions are called?

0 Answers0