← Back to branch summary

~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to tests/misc/dur.c

  • Committer: Bazaar Package Importer
  • Author(s): Mehdi Dogguy
  • Date: 2009-06-03 08:19:25 UTC
  • Revision ID: james.westby@ubuntu.com-20090603081925-kihvxvt0wy3zc4ar
Tags: upstream-20081201.dfsg
Import upstream version 20081201.dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
tests/misc/dur.c
 
1
/* run.config
 
2
  GCC:
 
3
  OPT: -memory-footprint 1 -val -deps -out -input  -main F2 -journal-disable
 
4
*/
 
5
 
 
6
struct T1 {
 
7
   float M1 ;
 
8
   unsigned short M2 ;
 
9
   unsigned short M3 ;
 
10
};
 
11
typedef struct T1 T2;
 
12
struct T3 {
 
13
   unsigned short M4 ;
 
14
   unsigned short M5 ;
 
15
};
 
16
typedef struct T3 T4;
 
17
struct T5 {
 
18
   float M6 ;
 
19
   float M7 ;
 
20
   float M8 ;
 
21
   float M9 ;
 
22
   float M10 ;
 
23
   float M11 ;
 
24
   float M12 ;
 
25
   float M13 ;
 
26
   float M14 ;
 
27
   float M15 ;
 
28
   float M16 ;
 
29
   float M17 ;
 
30
   float M18 ;
 
31
   float M19 ;
 
32
   float M20 ;
 
33
   float M21 ;
 
34
   float M22 ;
 
35
   float M23 ;
 
36
   float M24 ;
 
37
   float M25 ;
 
38
   float M26[(unsigned short)26] ;
 
39
   float M27[(unsigned short)13] ;
 
40
   float M28[(unsigned short)3] ;
 
41
   float M29 ;
 
42
   float M30 ;
 
43
   float M31 ;
 
44
   float M32 ;
 
45
   float M33 ;
 
46
   float M34 ;
 
47
   float M35 ;
 
48
   float M36 ;
 
49
   float M37 ;
 
50
   float M38 ;
 
51
   float M39 ;
 
52
   float M40 ;
 
53
   float M41 ;
 
54
   float M42 ;
 
55
   float M43 ;
 
56
   float M44 ;
 
57
   float M45 ;
 
58
   float M46 ;
 
59
   float M47 ;
 
60
   float M48 ;
 
61
   float M49 ;
 
62
   float M50 ;
 
63
   float M51 ;
 
64
   float M52 ;
 
65
   float M53 ;
 
66
   float M54 ;
 
67
   float M55 ;
 
68
   float M56 ;
 
69
   float M57 ;
 
70
   float M58 ;
 
71
   float M59 ;
 
72
   float M60 ;
 
73
   float M61 ;
 
74
   float M62 ;
 
75
   float M63 ;
 
76
   float M64[27] ;
 
77
   float M65[27] ;
 
78
   float M66[(unsigned short)48] ;
 
79
   float M67[(unsigned short)48] ;
 
80
   float M68[(unsigned short)48] ;
 
81
   float M69[(unsigned short)48] ;
 
82
   float M70[48] ;
 
83
   float M71[48] ;
 
84
   float M72[48] ;
 
85
   float M73[48] ;
 
86
   float M74[(unsigned short)10] ;
 
87
};
 
88
typedef struct T5 T6;
 
89
struct T7 {
 
90
   unsigned short M75 ;
 
91
   T2 M76[(unsigned short)53] ;
 
92
   T2 M77 ;
 
93
   T2 M78 ;
 
94
   T2 M79 ;
 
95
   T2 M80 ;
 
96
   T2 M81 ;
 
97
   T2 M82 ;
 
98
   T2 M83 ;
 
99
   T2 M84 ;
 
100
   T2 M85 ;
 
101
   T2 M86 ;
 
102
   T2 M87 ;
 
103
   T2 M88 ;
 
104
   T2 M89 ;
 
105
   T4 M90[(unsigned short)4] ;
 
106
   T4 M91 ;
 
107
   T2 M92[(unsigned short)6] ;
 
108
   T4 M93[(unsigned short)5] ;
 
109
};
 
110
typedef struct T7 T8;
 
111
struct T9 {
 
112
   unsigned short M94[(unsigned short)1][16] ;
 
113
   unsigned short M95[(unsigned short)1] ;
 
114
   unsigned short M96[(unsigned short)1] ;
 
115
   unsigned short M97[(unsigned short)1] ;
 
116
   unsigned short M98 ;
 
117
};
 
118
typedef struct T9 T10;
 
119
int G1 ;
 
120
int G2 ;
 
121
extern unsigned char G3 ;
 
122
extern T6 const   G4 ;
 
123
extern T8 G5 ;
 
124
extern T10 G6 ;
 
125
extern unsigned char G7[(unsigned short)161] ;
 
126
void F1(T2 *V1 , T2 *V2 , unsigned short const   V3 ,
 
127
        unsigned short const   V4 )
 
128
{
 
129
 
 
130
  {if ((int )V1->M2 != 0)
 
131
   {if ((int )V1->M2 == 2) {G7[V3] = (unsigned char)1;}
 
132
    else {G7[V3] = (unsigned char)0;}
 
133
 
 
134
   V1->M2 = (unsigned short)1;
 
135
   if ((int )V2->M2 == 0)
 
136
   {G7[V4] = (unsigned char)0;
 
137
   if (V2->M1 <= G4.M16) {G7[V3] = (unsigned char)1;
 
138
     if (V2->M1 <= G4.M17) {G7[V4] = (unsigned char)1;
 
139
       V2->M2 = (unsigned short)1;}
 
140
     }
 
141
   }
 
142
   else {G7[V4] = (unsigned char)1;
 
143
   V2->M2 = (unsigned short)1;}
 
144
   }
 
145
   else {G7[V3] = (unsigned char)0;
 
146
   V2->M2 = (unsigned short )((int )V2->M2 != 0);
 
147
   G7[V4] = (unsigned char )V2->M2;}
 
148
 
 
149
  return;}
 
150
 
 
151
}
 
152
void F2(unsigned short V8 )
 
153
{ unsigned short V5 ;
 
154
  unsigned short V6 ;
 
155
  unsigned short V7 ;
 
156
 
 
157
  {G5.M75 = (unsigned short )G3;
 
158
  if ((int )V8 == 0) {if ((((int )G6.M97[0] & 1) == 1) == 1)
 
159
                      {G5.M91.M4 = (unsigned short)0;
 
160
                      G5.M91.M5 = (unsigned short)1;}
 
161
                      else {G5.M91.M4 = (unsigned short )(((int )G6.M96[0] & 1) == 1);
 
162
                      G5.M91.M5 = (unsigned short)0;}
 
163
 
 
164
    V6 = (unsigned short)0;
 
165
    V7 = (unsigned short)2;
 
166
    V5 = (unsigned short)0;
 
167
    while ((int )V5 < 4) {if (G2)
 
168
                          {G5.M90[V5].M4 = (unsigned short)0;
 
169
                          G5.M90[V5].M5 = (unsigned short)1;}
 
170
                          else {G5.M90[V5].M4 = (unsigned short )G1;
 
171
                          if ((int )G5.M90[V5].M4 == 1) {V6 = (unsigned short )(
 
172
                                                         (int )V6 + 1);}
 
173
 
 
174
                          G5.M90[V5].M5 = (unsigned short)0;}
 
175
 
 
176
      V7 = (unsigned short )(2 * (int )V7);
 
177
      V5 = (unsigned short )((int )V5 + 1);}
 
178
    }
 
179
 
 
180
  return;}
 
181
 
 
182
}