ACSL "assigns" annotation for inner structs and fields of C code

Question

Suppose we have such a data structure:

#typedef struct
{
int  C_Field;
}C;

#typedef struct
{
C B_Array[MAX_SIZE];
}B;

#typedef struct
{
 B A_Array[MAX_SIZE];
}A;

It seems that Frama-C doesn’t assign a location for a field of a struct of type C in the following example:

/*@
  assigns Arg->A_Array[0..(MAX_SIZE - 1)].B_Array[0..(MAX_SIZE - 1)].C_Field;
*/
void Initialize (A * Arg);

Is the above annotation acceptable by Frama-C at all?

The code is elaborated as follows. The main goal is to reset the field C_Field to 0:

/*@ predicate 
      ResetB (B * Arg) =
        \forall integer Index; 0<= Index < MAX_SIZE ==>
                 Arg -> B_Array[Index].C_Field == 0;
*/

//@ assigns * Arg;
// Even I tried this:
//@ assigns Arg -> A_Array[0..(MAX_SIZE - 1)];
void Initialize (A * Arg)
{
 /*@ loop invariant 0 <= Index <= MAX_SIZE;
     loop invariant ResetB(&(Arg->A_Array[Index]));
     loop assigns Index, Arg -> A_Array[0..(MAX_SIZE - 1)];
 */
 for (int Index = 0; Index < MAX_SIZE; Index++)
  {
    Reset(&(Arg -> A_Array[Index]));
  }
}

/*@ assigns Arg -> B_Array[0..(MAX_SIZE - 1)];
    ensures ResetB(Arg);      
*/
void Reset(B * Arg)
{
 /*@ loop invariant 0 <= Index <= MAX_SIZE;
     loop invariant \forall integer i; 0<= i < Index ==>
                     Arg -> B_Array[i].C_Field == 0;
     loop assigns Index, Arg -> B_Array[0..(MAX_SIZE - 1)];
 */
 for (int Index = 0; Index < MAX_SIZE; Index++)
 {
  Arg -> B_Array[Index].C_Field = 0;
 }
}

The contract of the function Reset is satisfied but the contract of the function Initialize is not. How to write a correct "assigns" for the contract of Initialize?

Your question is a bit unclear. Frama-C Silicon (the latest stable version) can perfectly parse the `assigns` (provided the `#` in front of the `typedef` are removed and a definition for `MAX_SIZE` is given). Could you describe _exactly_ what you tried with this code and how the result given by Frama-C differ from what you expected? — Virgile, Apr 27 '17 at 06:23
Thanks for response. Our main goal is to reset the field C_Field to 0. The code above is elaborated as follows: — Rocolife, Apr 27 '17 at 07:04
Welcome to StackOverflow. Is this supposed to be C syntax? Then fix the syntax errors and/or strange mixups of preprocessor/compiler syntax. I think @Virgile meant the same. Then provide a [mcve]. Otherwise remove the C tag. And please consider taking the [tour]. — Yunnosch, Apr 27 '17 at 07:22
The code as shown seems far from being C-code. Can you compile, show the errors a c-compiler gives and comment on why you have problems with fixing them or do not want to? If making a compileable mcve is a problem for you, then get it as compileable as possible and ask about the one error you fail to fix. Please phrase you question so that it convinces readers that you did try to compile with a c-compiler. You can also make it compileable by "deactivating" the code line which cause errors (i.e. provide them as comments). — Yunnosch, Apr 27 '17 at 11:18
The main question is about the memory locations which are modified when a function is called. How to write the locations properly in the "assigns" annotation of ACSL? It seems the task is complex when the code consists of a couple of inner structs. Therefore, the question is not about the C code itself and compilation errors. — Rocolife, Apr 27 '17 at 11:33
@Rocolife If your code does not compile, there isn't much point to try to prove something about it. Moreover, your last sentence is still not precise enough. I'd assume that what you mean is "When I run `frama-c -wp file.c`, the contract of `Reset` is marked valid, while the contract of `Initialize` is not", but the plug-in you use should have been mentioned explicitely. There are many possible uses of Frama-C, and the answer to "Why isn't xxx proved?" will vary widely depending not only on xxx but also on the plug-ins you use. — Virgile, Apr 27 '17 at 11:57
Sorry for my short version of my code. Please look at the latest. The code is compiled without error. I'm using the WP plugin. As you said, the annotations of Reset are tagged with green bullet when I run frama-c -wp file.c. However, the annotations of Initialize are tagged with bi-color except the "assigns" and "loop assigns" which are tagged with yellow. Any help for the yellow part, please? — Rocolife, Apr 27 '17 at 12:53
In summary, which memory locations are modified after the function Initialize is called? — Rocolife, Apr 27 '17 at 13:28

Virgile · Accepted Answer · 2017-04-27T14:58:44.170

Assuming that you're using plugin WP (see comment above), your main issue is that you haven't written a loop assigns for your loop in the Initialize function. loop assigns are mandatory for each loop appearing in the function(s) over which you want to use WP. In addition, if your contract has ensures clauses, you'll very likely need loop invariant, again for every single loop in the code under analysis.

Update With the code you have provided, and frama-c Silicon, the only thing that is not proved with frama-c -wp file.c is the loop invariant in Initialize about ResetB. The reason why it is not proved is that it is wrong. The real invariant should read \forall integer i; 0<=i<Index ==> ResetB(&(Arg->A_Array[i])). With the following complete example, everything gets discharged, at least with Silicon:

#define MAX_SIZE 100

typedef struct
{
int  C_Field;
int D_Field;
}C;

typedef struct
{
C B_Array[MAX_SIZE];
}B;

typedef struct
{
 B A_Array[MAX_SIZE];
}A;

/*@ predicate 
      ResetB (B * Arg) =
        \forall integer Index; 0<= Index < MAX_SIZE ==>
                 Arg -> B_Array[Index].C_Field == 0;
*/

void Reset(B * Arg);

// @ assigns * Arg;
// Even I tried this:
//@ assigns Arg -> A_Array[0..(MAX_SIZE - 1)];
void Initialize (A * Arg)
{
 /*@ loop invariant 0 <= Index <= MAX_SIZE;
     loop invariant \forall integer i; 0<=i<Index ==> ResetB(&(Arg->A_Array[i]));
     loop assigns Index, Arg -> A_Array[0..(MAX_SIZE - 1)];
 */
 for (int Index = 0; Index < MAX_SIZE; Index++)
  {
    Reset(&(Arg -> A_Array[Index]));
  }
}

/*@ assigns Arg -> B_Array[0..(MAX_SIZE - 1)];
    ensures ResetB(Arg);
*/
void Reset(B * Arg)
{
 /*@ loop invariant 0 <= Index <= MAX_SIZE;
     loop invariant \forall integer i; 0<= i < Index ==>
                     Arg -> B_Array[i].C_Field == 0;
     loop assigns Index, Arg -> B_Array[0..(MAX_SIZE - 1)];
 */
 for (int Index = 0; Index < MAX_SIZE; Index++)
 {
  Arg -> B_Array[Index].C_Field = 0;
 }
}

The predicate has already a \forall. How come you use another \forall before the predicate in the loop invariant of Initialize? — Rocolife, Apr 27 '17 at 15:38
Sorry you're right. Your suggested invariant is for two nested "for" loops. That's exactly what is needed to get our verification done. Many thanks. — Rocolife, Apr 28 '17 at 04:07
@Rocolife Glad to have helped. If you think this answer was useful, don't hesitate to [accept it](https://stackoverflow.com/help/accepted-answer). — Virgile, Apr 28 '17 at 13:23

ACSL "assigns" annotation for inner structs and fields of C code

1 Answers1