//frama-c -wp source.c -wp-timeout 200


typedef struct {
  int c1;
//  int c2;
//  int c3;
//  int c4;
//  int c5;
//  int c6;
//  int c7;
//  int c8;
//  int c9;
  int p1[2];
} T_S1;

typedef struct {
  int c1;
  int c2;
  int c3;
  int c4;
  int c5;
  int c6;
  int c7;
  int c8;
  int c9;
  int p1[2];
} T_S2;

T_S1 GlobS1;
T_S2 GlobS2;

/*@
  assigns GlobS1, *s;
  ensures GlobS1 == *s;
*/
void g1(T_S1* s);

/*@
  ensures *p==GlobS1;
*/
void f1(T_S1* p)
{
  g1(p);
}

/*@
  assigns GlobS2, *s;
  ensures GlobS2 == *s;
*/
void g2(T_S2* s);

/*@
  ensures *p==GlobS2;
*/
void f2(T_S2* p)
{
  g2(p);
}