title: Shall we write "assert" after each function call when a sequence of functions are called?
body: <p>Let me start my question by this example: </p>
  
  <pre><code>void A (void)
  {
    B();
    C();
    D();
    E();
    ... // function calls go on.
  
    return;
  }
  </code></pre>
  
  <p>Now let's add ACSL annotations to the code:</p>
  
  <pre><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;
  }
  </code></pre>
  
  <p>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:</p>
  
  <pre><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;
  } 
  </code></pre>
  
  <p>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?</p>
  
  <p><strong>Updated Code:</strong></p>
  
  <p>The file.h looks as follows:</p>
  
  <pre><code>#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-&gt;Field_1 == 0) &amp;&amp;
     (Stct_B-&gt;Field_2 == 0) &amp;&amp;
     (Stct_B-&gt;Field_3 == 0) &amp;&amp;
     (Stct_B-&gt;Field_4 == 0);
  */
  
  /*@ predicate 
    Reset_At_1 (Struct_B * Stct_B, integer First, integer Last) =
      \forall integer Index; First &lt;= Index &lt; Last ==&gt;
                  (Stct_B-&gt;At_1 [ Index ].Field_5 == 0) &amp;&amp;
                  (Stct_B-&gt;At_1 [ Index ].Field_6 == 0);
  */
  
  
  /*@ predicate 
    Reset_At_2 (Struct_B * Stct_B, integer First, integer Last) =
      \forall integer Index; First &lt;= Index &lt; Last ==&gt;
                  (Stct_B-&gt;At_2 [ Index ].Field_5 == 0) &amp;&amp;
                  (Stct_B-&gt;At_2 [ Index ].Field_6 == 0);
  */
  
  /*@ predicate 
    Reset_At_3 (Struct_B * Stct_B, integer First, integer Last) =
      \forall integer Index; First &lt;= Index &lt; Last ==&gt;
                  (Stct_B-&gt;At_3 [ Index ].Field_5 == 0) &amp;&amp;
                  (Stct_B-&gt;At_3 [ Index ].Field_6 == 0);
  */
  </code></pre>
  
  <p>The file.c looks as follows: </p>
  
  <pre><code>#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-&gt;At [ 0..(SIZE_FIRST - 1) ];
     assigns Stct_A-&gt;Count;
  */
  void Initialize (Struct_A * const Stct_A)
  {
  
  /*@
   loop invariant 0 &lt;= Index &lt;= SIZE_FIRST;
  
   loop invariant \forall integer Stct_B_Index; (0 &lt;= Stct_B_Index &lt; 
        Index) ==&gt; Reset_Basics(&amp;(Stct_A-&gt;At [ Stct_B_Index ]));
  
   loop invariant \forall integer Stct_B_Index; (0 &lt;= Stct_B_Index &lt; 
        Index) ==&gt; Reset_At_1(&amp;(Stct_A-&gt;At [ Stct_B_Index ]), 0,   
        SIZE_SECOND);
  
   loop invariant \forall integer Stct_B_Index; (0 &lt;= Stct_B_Index &lt; 
        Index) ==&gt; Reset_At_2(&amp;(Stct_A-&gt;At [ Stct_B_Index ]), 0, 
        SIZE_THIRD);
  
   loop invariant \forall integer Stct_B_Index; (0 &lt;= Stct_B_Index &lt; 
        Index) ==&gt; Reset_At_3(&amp;(Stct_A-&gt;At [ Stct_B_Index ]), 0,
        SIZE_THIRD);
  
   loop assigns Index, Stct_A-&gt;At [ 0..(SIZE_FIRST - 1) ];
  
   loop variant SIZE_FIRST - Index;
  */
   for (int Index = 0; Index &lt; SIZE_FIRST; ++(Index))
    {
     Reset(&amp;(Stct_A-&gt;At [ Index ]));
    } 
  
    Stct_A-&gt;Count = 0;
  
   return;
   }
  
  /*@ 
    assigns * Stct_B;
    ensures Reset_Basics(Stct_B);
  */
  void Reset_Basics (Struct_B * const Stct_B) 
  {
  
    Stct_B-&gt;Field_1 = 0;
    Stct_B-&gt;Field_2 = 0;
    Stct_B-&gt;Field_3 = 0;
    Stct_B-&gt;Field_4 = 0;
  
    return; 
  }
  
  /*@
    assigns Stct_B-&gt;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 &lt;= Index &lt;= SIZE_SECOND;
  
   loop invariant Reset_At_1(Stct_B, 0, Index);
  
   loop assigns Index, Stct_B-&gt;At_1 [ 0..(SIZE_SECOND - 1) ];
  
   loop variant SIZE_SECOND - Index;
  */
    for (int Index = 0; Index &lt; SIZE_SECOND; ++(Index))
    {
      Stct_B-&gt;At_1 [ Index ].Field_5 = 0;
      Stct_B-&gt;At_1 [ Index ].Field_6 = 0;
    }
  
    return;
   }
  
  /*@ 
    assigns Stct_B-&gt;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 &lt;= Index &lt;= SIZE_THIRD;
  
     loop invariant Reset_At_2(Stct_B, 0, Index);
  
     loop assigns Index, Stct_B-&gt;At_2 [0..(SIZE_THIRD - 1)];
  
     loop variant SIZE_THIRD - Index; 
   */ 
    for (int Index = 0; Index &lt; SIZE_THIRD; ++(Index))
     {
       Stct_B-&gt;At_2 [ Index ].Field_5 = 0;
       Stct_B-&gt;At_2 [ Index ].Field_6 = 0;
     }  
  
      return;
   }
  
  
  /*@ 
     assigns Stct_B-&gt;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 &lt;= Index &lt;= SIZE_THIRD;
  
     loop invariant Reset_At_3(Stct_B, 0, Index);
  
     loop assigns Index, Stct_B-&gt;At_3 [0..(SIZE_THIRD - 1)];
  
     loop variant SIZE_THIRD - Index; 
     */ 
    for (int Index = 0; Index &lt; SIZE_THIRD; ++(Index))
     {
       Stct_B-&gt;At_3 [ Index ].Field_5 = 0;
       Stct_B-&gt;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;
  }
  </code></pre>