File: dur.i

package info (click to toggle)
frama-c 20161101%2Bsilicon%2Bdfsg-5
  • links: PTS, VCS
  • area: main
  • in suites: stretch
  • size: 42,324 kB
  • ctags: 35,695
  • sloc: ml: 200,142; ansic: 31,465; makefile: 2,334; sh: 1,643; lisp: 259; python: 85; asm: 26
file content (182 lines) | stat: -rw-r--r-- 3,977 bytes parent folder | download | duplicates (3)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
/* run.config*
  GCC:
  STDOPT: #"-float-normal -main F2"
*/

struct T1 {
   float M1 ;
   unsigned short M2 ;
   unsigned short M3 ;
};
typedef struct T1 T2;
struct T3 {
   unsigned short M4 ;
   unsigned short M5 ;
};
typedef struct T3 T4;
struct T5 {
   float M6 ;
   float M7 ;
   float M8 ;
   float M9 ;
   float M10 ;
   float M11 ;
   float M12 ;
   float M13 ;
   float M14 ;
   float M15 ;
   float M16 ;
   float M17 ;
   float M18 ;
   float M19 ;
   float M20 ;
   float M21 ;
   float M22 ;
   float M23 ;
   float M24 ;
   float M25 ;
   float M26[(unsigned short)26] ;
   float M27[(unsigned short)13] ;
   float M28[(unsigned short)3] ;
   float M29 ;
   float M30 ;
   float M31 ;
   float M32 ;
   float M33 ;
   float M34 ;
   float M35 ;
   float M36 ;
   float M37 ;
   float M38 ;
   float M39 ;
   float M40 ;
   float M41 ;
   float M42 ;
   float M43 ;
   float M44 ;
   float M45 ;
   float M46 ;
   float M47 ;
   float M48 ;
   float M49 ;
   float M50 ;
   float M51 ;
   float M52 ;
   float M53 ;
   float M54 ;
   float M55 ;
   float M56 ;
   float M57 ;
   float M58 ;
   float M59 ;
   float M60 ;
   float M61 ;
   float M62 ;
   float M63 ;
   float M64[27] ;
   float M65[27] ;
   float M66[(unsigned short)48] ;
   float M67[(unsigned short)48] ;
   float M68[(unsigned short)48] ;
   float M69[(unsigned short)48] ;
   float M70[48] ;
   float M71[48] ;
   float M72[48] ;
   float M73[48] ;
   float M74[(unsigned short)10] ;
};
typedef struct T5 T6;
struct T7 {
   unsigned short M75 ;
   T2 M76[(unsigned short)53] ;
   T2 M77 ;
   T2 M78 ;
   T2 M79 ;
   T2 M80 ;
   T2 M81 ;
   T2 M82 ;
   T2 M83 ;
   T2 M84 ;
   T2 M85 ;
   T2 M86 ;
   T2 M87 ;
   T2 M88 ;
   T2 M89 ;
   T4 M90[(unsigned short)4] ;
   T4 M91 ;
   T2 M92[(unsigned short)6] ;
   T4 M93[(unsigned short)5] ;
};
typedef struct T7 T8;
struct T9 {
   unsigned short M94[(unsigned short)1][16] ;
   unsigned short M95[(unsigned short)1] ;
   unsigned short M96[(unsigned short)1] ;
   unsigned short M97[(unsigned short)1] ;
   unsigned short M98 ;
};
typedef struct T9 T10;
int G1 ;
int G2 ;
extern unsigned char G3 ;
extern T6 const   G4 ;
extern T8 G5 ;
extern T10 G6 ;
extern unsigned char G7[(unsigned short)161] ;
void F1(T2 *V1 , T2 *V2 , unsigned short const   V3 ,
        unsigned short const   V4 )
{

  {if ((int )V1->M2 != 0)
   {if ((int )V1->M2 == 2) {G7[V3] = (unsigned char)1;}
    else {G7[V3] = (unsigned char)0;}

   V1->M2 = (unsigned short)1;
   if ((int )V2->M2 == 0)
   {G7[V4] = (unsigned char)0;
   if (V2->M1 <= G4.M16) {G7[V3] = (unsigned char)1;
     if (V2->M1 <= G4.M17) {G7[V4] = (unsigned char)1;
       V2->M2 = (unsigned short)1;}
     }
   }
   else {G7[V4] = (unsigned char)1;
   V2->M2 = (unsigned short)1;}
   }
   else {G7[V3] = (unsigned char)0;
   V2->M2 = (unsigned short )((int )V2->M2 != 0);
   G7[V4] = (unsigned char )V2->M2;}

  return;}

}
void F2(unsigned short V8 )
{ unsigned short V5 ;
  unsigned short V6 ;
  unsigned short V7 ;

  {G5.M75 = (unsigned short )G3;
  if ((int )V8 == 0) {if ((((int )G6.M97[0] & 1) == 1) == 1)
                      {G5.M91.M4 = (unsigned short)0;
                      G5.M91.M5 = (unsigned short)1;}
                      else {G5.M91.M4 = (unsigned short )(((int )G6.M96[0] & 1) == 1);
                      G5.M91.M5 = (unsigned short)0;}

    V6 = (unsigned short)0;
    V7 = (unsigned short)2;
    V5 = (unsigned short)0;
    while ((int )V5 < 4) {if (G2)
                          {G5.M90[V5].M4 = (unsigned short)0;
                          G5.M90[V5].M5 = (unsigned short)1;}
                          else {G5.M90[V5].M4 = (unsigned short )G1;
                          if ((int )G5.M90[V5].M4 == 1) {V6 = (unsigned short )(
                                                         (int )V6 + 1);}

                          G5.M90[V5].M5 = (unsigned short)0;}

      V7 = (unsigned short )(2 * (int )V7);
      V5 = (unsigned short )((int )V5 + 1);}
    }

  return;}

}