Project

General

Profile

« Previous | Next » 

Revision 97602f7c

Added by Guillaume Davy over 9 years ago

Correct bug when there is no precondition and change reprensentation
of boolean in ACSL

View differences:

tcm_benchmarks/ALT2/ALT2_proof/ALT_2.lustrec.c
26 26
                           double hdot_Out1_59, double hdotChgRate_Out1_69, 
27 27
                           double (*altgammacmd_In1_661),
28 28
                           struct AltitudeControl_mem *self) {
29
  /*@ensures Ctrans_AltitudeControl(AntEng_Out1_19,
30
                                    AltCmd_Out1_29,
31
                                    Alt_Out1_39,
32
                                    GsKts_Out1_49,
33
                                    hdot_Out1_59,
34
                                    hdotChgRate_Out1_69,
35
                                    *altgammacmd_In1_661,
29
  /*@ensures Ctrans_AltitudeControl((AntEng_Out1_19),
30
                                    (AltCmd_Out1_29),
31
                                    (Alt_Out1_39),
32
                                    (GsKts_Out1_49),
33
                                    (hdot_Out1_59),
34
                                    (hdotChgRate_Out1_69),
35
                                    (*altgammacmd_In1_661),
36 36
                                    \at(*self, Pre),
37 37
                                    (*self));
38 38
  assigns *altgammacmd_In1_661, *self;
......
63 63
  /*@ensures \exists real Saturation1_Out1_213;
64 64
  \exists real Variable_Limit_Saturation_0_Out1_509;
65 65
  \exists real Variable__Rate_Limit_Out1_324;
66
  trans_AltitudeControl(AntEng_Out1_19,
67
                        AltCmd_Out1_29,
68
                        Alt_Out1_39,
69
                        GsKts_Out1_49,
70
                        hdot_Out1_59,
71
                        hdotChgRate_Out1_69,
72
                        *altgammacmd_In1_661,
66
  trans_AltitudeControl((AntEng_Out1_19),
67
                        (AltCmd_Out1_29),
68
                        (Alt_Out1_39),
69
                        (GsKts_Out1_49),
70
                        (hdot_Out1_59),
71
                        (hdotChgRate_Out1_69),
72
                        (*altgammacmd_In1_661),
73 73
                        \at(*self, Pre),
74 74
                        (*self),
75
                        Abs_Out1_144,
76
                        Kh_Out1_193,
77
                        Logical_Operator_In1_197,
78
                        Logical_Operator_Out1_198,
79
                        Saturation1_Out1_213,
80
                        Sum3_Out1_296,
81
                        Sum_Out1_286,
82
                        Switch1_In2_312,
83
                        Switch1_Out1_314,
84
                        Switch_In2_303,
85
                        Switch_Out1_305,
86
                        Variable_Limit_Saturation_0_Out1_509,
87
                        Variable__Rate_Limit_Out1_324,
88
                        __AltitudeControl_1,
89
                        __AltitudeControl_2,
90
                        k_Out1_585,
91
                        kts2fps_Out1_594,
92
                        r2d_Out1_603);
75
                        (Abs_Out1_144),
76
                        (Kh_Out1_193),
77
                        (Logical_Operator_In1_197?\true:\false),
78
                        (Logical_Operator_Out1_198?\true:\false),
79
                        (Saturation1_Out1_213),
80
                        (Sum3_Out1_296),
81
                        (Sum_Out1_286),
82
                        (Switch1_In2_312?\true:\false),
83
                        (Switch1_Out1_314),
84
                        (Switch_In2_303?\true:\false),
85
                        (Switch_Out1_305),
86
                        (Variable_Limit_Saturation_0_Out1_509),
87
                        (Variable__Rate_Limit_Out1_324),
88
                        (__AltitudeControl_1?\true:\false),
89
                        (__AltitudeControl_2?\true:\false),
90
                        (k_Out1_585),
91
                        (kts2fps_Out1_594),
92
                        (r2d_Out1_603));
93 93
  assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193,
94 94
          Logical_Operator_In1_197, Logical_Operator_Out1_198,
95 95
          Saturation1_Out1_213, Sum3_Out1_296, Sum_Out1_286, Switch1_In2_312,
......
102 102
  
103 103
  /*@ensures \exists real Variable_Limit_Saturation_0_Out1_509;
104 104
  \exists real Variable__Rate_Limit_Out1_324;
105
  trans_AltitudeControl(AntEng_Out1_19,
106
                        AltCmd_Out1_29,
107
                        Alt_Out1_39,
108
                        GsKts_Out1_49,
109
                        hdot_Out1_59,
110
                        hdotChgRate_Out1_69,
111
                        *altgammacmd_In1_661,
105
  trans_AltitudeControl((AntEng_Out1_19),
106
                        (AltCmd_Out1_29),
107
                        (Alt_Out1_39),
108
                        (GsKts_Out1_49),
109
                        (hdot_Out1_59),
110
                        (hdotChgRate_Out1_69),
111
                        (*altgammacmd_In1_661),
112 112
                        \at(*self, Pre),
113 113
                        (*self),
114
                        Abs_Out1_144,
115
                        Kh_Out1_193,
116
                        Logical_Operator_In1_197,
117
                        Logical_Operator_Out1_198,
118
                        Saturation1_Out1_213,
119
                        Sum3_Out1_296,
120
                        Sum_Out1_286,
121
                        Switch1_In2_312,
122
                        Switch1_Out1_314,
123
                        Switch_In2_303,
124
                        Switch_Out1_305,
125
                        Variable_Limit_Saturation_0_Out1_509,
126
                        Variable__Rate_Limit_Out1_324,
127
                        __AltitudeControl_1,
128
                        __AltitudeControl_2,
129
                        k_Out1_585,
130
                        kts2fps_Out1_594,
131
                        r2d_Out1_603);
114
                        (Abs_Out1_144),
115
                        (Kh_Out1_193),
116
                        (Logical_Operator_In1_197?\true:\false),
117
                        (Logical_Operator_Out1_198?\true:\false),
118
                        (Saturation1_Out1_213),
119
                        (Sum3_Out1_296),
120
                        (Sum_Out1_286),
121
                        (Switch1_In2_312?\true:\false),
122
                        (Switch1_Out1_314),
123
                        (Switch_In2_303?\true:\false),
124
                        (Switch_Out1_305),
125
                        (Variable_Limit_Saturation_0_Out1_509),
126
                        (Variable__Rate_Limit_Out1_324),
127
                        (__AltitudeControl_1?\true:\false),
128
                        (__AltitudeControl_2?\true:\false),
129
                        (k_Out1_585),
130
                        (kts2fps_Out1_594),
131
                        (r2d_Out1_603));
132 132
  assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193,
133 133
          Logical_Operator_In1_197, Logical_Operator_Out1_198,
134 134
          Saturation1_Out1_213, Sum3_Out1_296, Sum_Out1_286, Switch1_In2_312,
......
140 140
  {
141 141
  
142 142
  /*@ensures \exists real Variable__Rate_Limit_Out1_324;
143
  trans_AltitudeControl(AntEng_Out1_19,
144
                        AltCmd_Out1_29,
145
                        Alt_Out1_39,
146
                        GsKts_Out1_49,
147
                        hdot_Out1_59,
148
                        hdotChgRate_Out1_69,
149
                        *altgammacmd_In1_661,
143
  trans_AltitudeControl((AntEng_Out1_19),
144
                        (AltCmd_Out1_29),
145
                        (Alt_Out1_39),
146
                        (GsKts_Out1_49),
147
                        (hdot_Out1_59),
148
                        (hdotChgRate_Out1_69),
149
                        (*altgammacmd_In1_661),
150 150
                        \at(*self, Pre),
151 151
                        (*self),
152
                        Abs_Out1_144,
153
                        Kh_Out1_193,
154
                        Logical_Operator_In1_197,
155
                        Logical_Operator_Out1_198,
156
                        Saturation1_Out1_213,
157
                        Sum3_Out1_296,
158
                        Sum_Out1_286,
159
                        Switch1_In2_312,
160
                        Switch1_Out1_314,
161
                        Switch_In2_303,
162
                        Switch_Out1_305,
163
                        Variable_Limit_Saturation_0_Out1_509,
164
                        Variable__Rate_Limit_Out1_324,
165
                        __AltitudeControl_1,
166
                        __AltitudeControl_2,
167
                        k_Out1_585,
168
                        kts2fps_Out1_594,
169
                        r2d_Out1_603);
152
                        (Abs_Out1_144),
153
                        (Kh_Out1_193),
154
                        (Logical_Operator_In1_197?\true:\false),
155
                        (Logical_Operator_Out1_198?\true:\false),
156
                        (Saturation1_Out1_213),
157
                        (Sum3_Out1_296),
158
                        (Sum_Out1_286),
159
                        (Switch1_In2_312?\true:\false),
160
                        (Switch1_Out1_314),
161
                        (Switch_In2_303?\true:\false),
162
                        (Switch_Out1_305),
163
                        (Variable_Limit_Saturation_0_Out1_509),
164
                        (Variable__Rate_Limit_Out1_324),
165
                        (__AltitudeControl_1?\true:\false),
166
                        (__AltitudeControl_2?\true:\false),
167
                        (k_Out1_585),
168
                        (kts2fps_Out1_594),
169
                        (r2d_Out1_603));
170 170
  assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193,
171 171
          Logical_Operator_In1_197, Logical_Operator_Out1_198,
172 172
          Saturation1_Out1_213, Sum3_Out1_296, Sum_Out1_286, Switch1_In2_312,
......
177 177
  */
178 178
  {
179 179
  
180
  /*@ensures trans_AltitudeControl(AntEng_Out1_19,
181
                                   AltCmd_Out1_29,
182
                                   Alt_Out1_39,
183
                                   GsKts_Out1_49,
184
                                   hdot_Out1_59,
185
                                   hdotChgRate_Out1_69,
186
                                   *altgammacmd_In1_661,
180
  /*@ensures trans_AltitudeControl((AntEng_Out1_19),
181
                                   (AltCmd_Out1_29),
182
                                   (Alt_Out1_39),
183
                                   (GsKts_Out1_49),
184
                                   (hdot_Out1_59),
185
                                   (hdotChgRate_Out1_69),
186
                                   (*altgammacmd_In1_661),
187 187
                                   \at(*self, Pre),
188 188
                                   (*self),
189
                                   Abs_Out1_144,
190
                                   Kh_Out1_193,
191
                                   Logical_Operator_In1_197,
192
                                   Logical_Operator_Out1_198,
193
                                   Saturation1_Out1_213,
194
                                   Sum3_Out1_296,
195
                                   Sum_Out1_286,
196
                                   Switch1_In2_312,
197
                                   Switch1_Out1_314,
198
                                   Switch_In2_303,
199
                                   Switch_Out1_305,
200
                                   Variable_Limit_Saturation_0_Out1_509,
201
                                   Variable__Rate_Limit_Out1_324,
202
                                   __AltitudeControl_1,
203
                                   __AltitudeControl_2,
204
                                   k_Out1_585,
205
                                   kts2fps_Out1_594,
206
                                   r2d_Out1_603);
189
                                   (Abs_Out1_144),
190
                                   (Kh_Out1_193),
191
                                   (Logical_Operator_In1_197?\true:\false),
192
                                   (Logical_Operator_Out1_198?\true:\false),
193
                                   (Saturation1_Out1_213),
194
                                   (Sum3_Out1_296),
195
                                   (Sum_Out1_286),
196
                                   (Switch1_In2_312?\true:\false),
197
                                   (Switch1_Out1_314),
198
                                   (Switch_In2_303?\true:\false),
199
                                   (Switch_Out1_305),
200
                                   (Variable_Limit_Saturation_0_Out1_509),
201
                                   (Variable__Rate_Limit_Out1_324),
202
                                   (__AltitudeControl_1?\true:\false),
203
                                   (__AltitudeControl_2?\true:\false),
204
                                   (k_Out1_585),
205
                                   (kts2fps_Out1_594),
206
                                   (r2d_Out1_603));
207 207
  assigns *altgammacmd_In1_661, *self, Abs_Out1_144, Kh_Out1_193,
208 208
          Logical_Operator_In1_197, Logical_Operator_Out1_198,
209 209
          Saturation1_Out1_213, Sum3_Out1_296, Sum_Out1_286, Switch1_In2_312,
......
216 216
  
217 217
  
218 218
  /*@
219
  ensures (__AltitudeControl_1 == (hdot_Out1_59 < 0.));
219
  ensures ((__AltitudeControl_1?\true:\false) == ((hdot_Out1_59) < 0.));
220 220
  assigns __AltitudeControl_1;
221 221
  */
222 222
  {
223 223
  __AltitudeControl_1 = (hdot_Out1_59 < 0.);
224 224
  }
225 225
  /*@
226
  ensures (Abs_Out1_144 == (__AltitudeControl_1?((- hdot_Out1_59)):(hdot_Out1_59)));
226
  ensures ((Abs_Out1_144) == ((__AltitudeControl_1?\true:\false)?((- (hdot_Out1_59))):((hdot_Out1_59))));
227 227
  assigns Abs_Out1_144;
228 228
  */
229 229
  {
230 230
  Abs_Out1_144 = (__AltitudeControl_1?((- hdot_Out1_59)):(hdot_Out1_59));
231 231
  }
232 232
  /*@
233
  ensures (Sum3_Out1_296 == (Abs_Out1_144 + 10.));
233
  ensures ((Sum3_Out1_296) == ((Abs_Out1_144) + 10.));
234 234
  assigns Sum3_Out1_296;
235 235
  */
236 236
  {
237 237
  Sum3_Out1_296 = (Abs_Out1_144 + 10.);
238 238
  }
239 239
  /*@
240
  ensures (k_Out1_585 == (- Sum3_Out1_296));
240
  ensures ((k_Out1_585) == (- (Sum3_Out1_296)));
241 241
  assigns k_Out1_585;
242 242
  */
243 243
  {
244 244
  k_Out1_585 = (- Sum3_Out1_296);
245 245
  }
246 246
  /*@
247
  ensures (__AltitudeControl_2 == (AntEng_Out1_19 == 0.));
247
  ensures ((__AltitudeControl_2?\true:\false) == ((AntEng_Out1_19) == 0.));
248 248
  assigns __AltitudeControl_2;
249 249
  */
250 250
  {
251 251
  __AltitudeControl_2 = (AntEng_Out1_19 == 0.);
252 252
  }
253 253
  /*@
254
  ensures ((!Logical_Operator_In1_197) == (!(__AltitudeControl_2?(0):(1))));
254
  ensures ((!(Logical_Operator_In1_197?\true:\false)) == (!((__AltitudeControl_2?\true:\false)?(0):(1))));
255 255
  assigns Logical_Operator_In1_197;
256 256
  */
257 257
  {
258 258
  Logical_Operator_In1_197 = (__AltitudeControl_2?(0):(1));
259 259
  }
260 260
  /*@
261
  ensures ((!Logical_Operator_Out1_198) == (!(!Logical_Operator_In1_197)));
261
  ensures ((!(Logical_Operator_Out1_198?\true:\false)) == (!(!(Logical_Operator_In1_197?\true:\false))));
262 262
  assigns Logical_Operator_Out1_198;
263 263
  */
264 264
  {
265 265
  Logical_Operator_Out1_198 = (!Logical_Operator_In1_197);
266 266
  }
267 267
  /*@
268
  ensures ((!Switch_In2_303) == (!(__AltitudeControl_2?(0):(1))));
268
  ensures ((!(Switch_In2_303?\true:\false)) == (!((__AltitudeControl_2?\true:\false)?(0):(1))));
269 269
  assigns Switch_In2_303;
270 270
  */
271 271
  {
272 272
  Switch_In2_303 = (__AltitudeControl_2?(0):(1));
273 273
  }
274 274
  /*@
275
  ensures (Sum_Out1_286 == (AltCmd_Out1_29 + (- Alt_Out1_39)));
275
  ensures ((Sum_Out1_286) == ((AltCmd_Out1_29) + (- (Alt_Out1_39))));
276 276
  assigns Sum_Out1_286;
277 277
  */
278 278
  {
279 279
  Sum_Out1_286 = (AltCmd_Out1_29 + (- Alt_Out1_39));
280 280
  }
281 281
  /*@
282
  ensures (Kh_Out1_193 == (0.08 * Sum_Out1_286));
282
  ensures ((Kh_Out1_193) == (0.08 * (Sum_Out1_286)));
283 283
  assigns Kh_Out1_193;
284 284
  */
285 285
  {
286 286
  Kh_Out1_193 = (0.08 * Sum_Out1_286);
287 287
  }
288 288
  /*@
289
  ensures (Switch_Out1_305 == (Switch_In2_303?(Kh_Out1_193):(0.)));
289
  ensures ((Switch_Out1_305) == ((Switch_In2_303?\true:\false)?((Kh_Out1_193)):(0.)));
290 290
  assigns Switch_Out1_305;
291 291
  */
292 292
  {
293 293
  Switch_Out1_305 = (Switch_In2_303?(Kh_Out1_193):(0.));
294 294
  }
295 295
  /*@
296
  ensures Ctrans_VariableLimitSaturation((double) Sum3_Out1_296,
297
                                         (double) Switch_Out1_305,
298
                                         (double) k_Out1_585,
299
                                         Variable_Limit_Saturation_0_Out1_509);
296
  ensures Ctrans_VariableLimitSaturation((Sum3_Out1_296),
297
                                         (Switch_Out1_305),
298
                                         (k_Out1_585),
299
                                         (Variable_Limit_Saturation_0_Out1_509));
300 300
  assigns Variable_Limit_Saturation_0_Out1_509;
301 301
  */
302 302
  {
303 303
  VariableLimitSaturation_step (Sum3_Out1_296, Switch_Out1_305, k_Out1_585, &Variable_Limit_Saturation_0_Out1_509);
304 304
  }
305 305
  /*@
306
  ensures Ctrans_VariableRateLimit((double) hdotChgRate_Out1_69,
307
                                   (double) Variable_Limit_Saturation_0_Out1_509,
308
                                   (_Bool) Logical_Operator_Out1_198,
309
                                   (double) hdot_Out1_59,
310
                                   Variable__Rate_Limit_Out1_324,
306
  ensures Ctrans_VariableRateLimit((hdotChgRate_Out1_69),
307
                                   (Variable_Limit_Saturation_0_Out1_509),
308
                                   (Logical_Operator_Out1_198?\true:\false),
309
                                   (hdot_Out1_59),
310
                                   (Variable__Rate_Limit_Out1_324),
311 311
                                   \at(*self, Pre).ni_0,
312 312
                                   (*self).ni_0);
313 313
  assigns Variable__Rate_Limit_Out1_324, \at(*self, Pre).ni_0, (*self).ni_0;
......
316 316
  VariableRateLimit_step (hdotChgRate_Out1_69, Variable_Limit_Saturation_0_Out1_509, Logical_Operator_Out1_198, hdot_Out1_59, &Variable__Rate_Limit_Out1_324, &self->ni_0);
317 317
  }
318 318
  /*@
319
  ensures (r2d_Out1_603 == (57.2958 * Variable__Rate_Limit_Out1_324));
319
  ensures ((r2d_Out1_603) == (57.2958 * (Variable__Rate_Limit_Out1_324)));
320 320
  assigns r2d_Out1_603;
321 321
  */
322 322
  {
323 323
  r2d_Out1_603 = (57.2958 * Variable__Rate_Limit_Out1_324);
324 324
  }
325 325
  /*@
326
  ensures (kts2fps_Out1_594 == (1.6878 * GsKts_Out1_49));
326
  ensures ((kts2fps_Out1_594) == (1.6878 * (GsKts_Out1_49)));
327 327
  assigns kts2fps_Out1_594;
328 328
  */
329 329
  {
330 330
  kts2fps_Out1_594 = (1.6878 * GsKts_Out1_49);
331 331
  }
332 332
  /*@
333
  ensures ((!Switch1_In2_312) == (!(__AltitudeControl_2?(0):(1))));
333
  ensures ((!(Switch1_In2_312?\true:\false)) == (!((__AltitudeControl_2?\true:\false)?(0):(1))));
334 334
  assigns Switch1_In2_312;
335 335
  */
336 336
  {
337 337
  Switch1_In2_312 = (__AltitudeControl_2?(0):(1));
338 338
  }
339 339
  /*@
340
  ensures (Switch1_Out1_314 == (Switch1_In2_312?(r2d_Out1_603):(0.)));
340
  ensures ((Switch1_Out1_314) == ((Switch1_In2_312?\true:\false)?((r2d_Out1_603)):(0.)));
341 341
  assigns Switch1_Out1_314;
342 342
  */
343 343
  {
344 344
  Switch1_Out1_314 = (Switch1_In2_312?(r2d_Out1_603):(0.));
345 345
  }
346 346
  /*@
347
  ensures (*altgammacmd_In1_661 == Switch1_Out1_314);
347
  ensures ((*altgammacmd_In1_661) == (Switch1_Out1_314));
348 348
  assigns *altgammacmd_In1_661;
349 349
  */
350 350
  {
351 351
  *altgammacmd_In1_661 = Switch1_Out1_314;
352 352
  }
353 353
  /*@
354
  ensures Ctrans_Saturation((double) kts2fps_Out1_594,
355
                            Saturation1_Out1_213);
354
  ensures Ctrans_Saturation((kts2fps_Out1_594),
355
                            (Saturation1_Out1_213));
356 356
  assigns Saturation1_Out1_213;
357 357
  */
358 358
  {
......
383 383
                             _Bool ICtrig_Out1_354, double IC_Out1_364, 
384 384
                             double (*output_In1_489),
385 385
                             struct VariableRateLimit_mem *self) {
386
  /*@ensures Ctrans_VariableRateLimit(ratelim_Out1_334,
387
                                      input_Out1_344,
388
                                      ICtrig_Out1_354,
389
                                      IC_Out1_364,
390
                                      *output_In1_489,
386
  /*@ensures Ctrans_VariableRateLimit((ratelim_Out1_334),
387
                                      (input_Out1_344),
388
                                      (ICtrig_Out1_354?\true:\false),
389
                                      (IC_Out1_364),
390
                                      (*output_In1_489),
391 391
                                      \at(*self, Pre),
392 392
                                      (*self));
393 393
  assigns *output_In1_489, *self;
......
406 406
  /* Asserting trans predicate: locals are [Variable_Limit_Saturation_Out1_410: real, __VariableRateLimit_2: real] */
407 407
  /*@ensures \exists real Variable_Limit_Saturation_Out1_410;
408 408
  \exists real __VariableRateLimit_2;
409
  trans_VariableRateLimit(ratelim_Out1_334,
410
                          input_Out1_344,
411
                          ICtrig_Out1_354,
412
                          IC_Out1_364,
413
                          *output_In1_489,
409
  trans_VariableRateLimit((ratelim_Out1_334),
410
                          (input_Out1_344),
411
                          (ICtrig_Out1_354?\true:\false),
412
                          (IC_Out1_364),
413
                          (*output_In1_489),
414 414
                          \at(*self, Pre),
415 415
                          (*self),
416
                          Gain1_Out1_382,
417
                          Gain_Out1_373,
418
                          Integrator1_Out1_391,
419
                          Sum2_Out1_401,
420
                          Variable_Limit_Saturation_Out1_410,
421
                          __VariableRateLimit_1,
422
                          __VariableRateLimit_2);
416
                          (Gain1_Out1_382),
417
                          (Gain_Out1_373),
418
                          (Integrator1_Out1_391),
419
                          (Sum2_Out1_401),
420
                          (Variable_Limit_Saturation_Out1_410),
421
                          (__VariableRateLimit_1?\true:\false),
422
                          (__VariableRateLimit_2));
423 423
  assigns *output_In1_489, *self, Gain1_Out1_382, Gain_Out1_373,
424 424
          Integrator1_Out1_391, Sum2_Out1_401,
425 425
          Variable_Limit_Saturation_Out1_410, __VariableRateLimit_1,
......
428 428
  {
429 429
  
430 430
  /*@ensures \exists real __VariableRateLimit_2;
431
  trans_VariableRateLimit(ratelim_Out1_334,
432
                          input_Out1_344,
433
                          ICtrig_Out1_354,
434
                          IC_Out1_364,
435
                          *output_In1_489,
431
  trans_VariableRateLimit((ratelim_Out1_334),
432
                          (input_Out1_344),
433
                          (ICtrig_Out1_354?\true:\false),
434
                          (IC_Out1_364),
435
                          (*output_In1_489),
436 436
                          \at(*self, Pre),
437 437
                          (*self),
438
                          Gain1_Out1_382,
439
                          Gain_Out1_373,
440
                          Integrator1_Out1_391,
441
                          Sum2_Out1_401,
442
                          Variable_Limit_Saturation_Out1_410,
443
                          __VariableRateLimit_1,
444
                          __VariableRateLimit_2);
438
                          (Gain1_Out1_382),
439
                          (Gain_Out1_373),
440
                          (Integrator1_Out1_391),
441
                          (Sum2_Out1_401),
442
                          (Variable_Limit_Saturation_Out1_410),
443
                          (__VariableRateLimit_1?\true:\false),
444
                          (__VariableRateLimit_2));
445 445
  assigns *output_In1_489, *self, Gain1_Out1_382, Gain_Out1_373,
446 446
          Integrator1_Out1_391, Sum2_Out1_401,
447 447
          Variable_Limit_Saturation_Out1_410, __VariableRateLimit_1,
......
449 449
  */
450 450
  {
451 451
  
452
  /*@ensures trans_VariableRateLimit(ratelim_Out1_334,
453
                                     input_Out1_344,
454
                                     ICtrig_Out1_354,
455
                                     IC_Out1_364,
456
                                     *output_In1_489,
452
  /*@ensures trans_VariableRateLimit((ratelim_Out1_334),
453
                                     (input_Out1_344),
454
                                     (ICtrig_Out1_354?\true:\false),
455
                                     (IC_Out1_364),
456
                                     (*output_In1_489),
457 457
                                     \at(*self, Pre),
458 458
                                     (*self),
459
                                     Gain1_Out1_382,
460
                                     Gain_Out1_373,
461
                                     Integrator1_Out1_391,
462
                                     Sum2_Out1_401,
463
                                     Variable_Limit_Saturation_Out1_410,
464
                                     __VariableRateLimit_1,
465
                                     __VariableRateLimit_2);
459
                                     (Gain1_Out1_382),
460
                                     (Gain_Out1_373),
461
                                     (Integrator1_Out1_391),
462
                                     (Sum2_Out1_401),
463
                                     (Variable_Limit_Saturation_Out1_410),
464
                                     (__VariableRateLimit_1?\true:\false),
465
                                     (__VariableRateLimit_2));
466 466
  assigns *output_In1_489, *self, Gain1_Out1_382, Gain_Out1_373,
467 467
          Integrator1_Out1_391, Sum2_Out1_401,
468 468
          Variable_Limit_Saturation_Out1_410, __VariableRateLimit_1,
......
472 472
  
473 473
  
474 474
  /*@
475
  ensures (__VariableRateLimit_1==(\at(*self, Pre).ni_2._reg._first?(1):(0))) && ((*self).ni_2._reg._first==0);
475
  ensures ((__VariableRateLimit_1?\true:\false)==(\at(*self, Pre).ni_2._reg._first?(1):(0))) && ((*self).ni_2._reg._first==0);
476 476
  assigns __VariableRateLimit_1, (*self).ni_2;
477 477
  */
478 478
  {
479 479
  _arrow_step (1, 0, &__VariableRateLimit_1, &self->ni_2);
480 480
  }
481 481
  /*@
482
  ensures (Integrator1_Out1_391 == (__VariableRateLimit_1?(IC_Out1_364):(\at(*self, Pre)._reg.__VariableRateLimit_3)));
482
  ensures ((Integrator1_Out1_391) == ((__VariableRateLimit_1?\true:\false)?((IC_Out1_364)):(\at(*self, Pre)._reg.__VariableRateLimit_3)));
483 483
  assigns Integrator1_Out1_391;
484 484
  */
485 485
  {
486 486
  Integrator1_Out1_391 = (__VariableRateLimit_1?(IC_Out1_364):(self->_reg.__VariableRateLimit_3));
487 487
  }
488 488
  /*@
489
  ensures (*output_In1_489 == Integrator1_Out1_391);
489
  ensures ((*output_In1_489) == (Integrator1_Out1_391));
490 490
  assigns *output_In1_489;
491 491
  */
492 492
  {
493 493
  *output_In1_489 = Integrator1_Out1_391;
494 494
  }
495 495
  /*@
496
  ensures (Gain1_Out1_382 == (- ratelim_Out1_334));
496
  ensures ((Gain1_Out1_382) == (- (ratelim_Out1_334)));
497 497
  assigns Gain1_Out1_382;
498 498
  */
499 499
  {
500 500
  Gain1_Out1_382 = (- ratelim_Out1_334);
501 501
  }
502 502
  /*@
503
  ensures (Sum2_Out1_401 == (input_Out1_344 + (- Integrator1_Out1_391)));
503
  ensures ((Sum2_Out1_401) == ((input_Out1_344) + (- (Integrator1_Out1_391))));
504 504
  assigns Sum2_Out1_401;
505 505
  */
506 506
  {
507 507
  Sum2_Out1_401 = (input_Out1_344 + (- Integrator1_Out1_391));
508 508
  }
509 509
  /*@
510
  ensures (Gain_Out1_373 == (20. * Sum2_Out1_401));
510
  ensures ((Gain_Out1_373) == (20. * (Sum2_Out1_401)));
511 511
  assigns Gain_Out1_373;
512 512
  */
513 513
  {
514 514
  Gain_Out1_373 = (20. * Sum2_Out1_401);
515 515
  }
516 516
  /*@
517
  ensures Ctrans_VariableLimitSaturation((double) ratelim_Out1_334,
518
                                         (double) Gain_Out1_373,
519
                                         (double) Gain1_Out1_382,
520
                                         Variable_Limit_Saturation_Out1_410);
517
  ensures Ctrans_VariableLimitSaturation((ratelim_Out1_334),
518
                                         (Gain_Out1_373),
519
                                         (Gain1_Out1_382),
520
                                         (Variable_Limit_Saturation_Out1_410));
521 521
  assigns Variable_Limit_Saturation_Out1_410;
522 522
  */
523 523
  {
524 524
  VariableLimitSaturation_step (ratelim_Out1_334, Gain_Out1_373, Gain1_Out1_382, &Variable_Limit_Saturation_Out1_410);
525 525
  }
526 526
  /*@
527
  ensures Ctrans_integrator_reset((double) Variable_Limit_Saturation_Out1_410,
528
                                  (_Bool) ICtrig_Out1_354,
529
                                  (double) IC_Out1_364,
530
                                  __VariableRateLimit_2,
527
  ensures Ctrans_integrator_reset((Variable_Limit_Saturation_Out1_410),
528
                                  (ICtrig_Out1_354?\true:\false),
529
                                  (IC_Out1_364),
530
                                  (__VariableRateLimit_2),
531 531
                                  \at(*self, Pre).ni_1,
532 532
                                  (*self).ni_1);
533 533
  assigns __VariableRateLimit_2, \at(*self, Pre).ni_1, (*self).ni_1;
......
536 536
  integrator_reset_step (Variable_Limit_Saturation_Out1_410, ICtrig_Out1_354, IC_Out1_364, &__VariableRateLimit_2, &self->ni_1);
537 537
  }
538 538
  /*@
539
  ensures ((*self)._reg.__VariableRateLimit_3 == __VariableRateLimit_2);
539
  ensures ((*self)._reg.__VariableRateLimit_3 == (__VariableRateLimit_2));
540 540
  assigns (*self)._reg.__VariableRateLimit_3;
541 541
  */
542 542
  {
......
548 548
void Saturation_step (double Signal, 
549 549
                      double (*s_out)
550 550
                      ) {
551
  /*@ensures Ctrans_Saturation(Signal,
552
                               *s_out);
551
  /*@ensures Ctrans_Saturation((Signal),
552
                               (*s_out));
553 553
  assigns *s_out;
554 554
  */
555 555
  {
......
560 560
  
561 561
  
562 562
  /* Asserting trans predicate: locals are [] */
563
  /*@ensures trans_Saturation(Signal,
564
                              *s_out,
565
                              __Saturation_1,
566
                              __Saturation_2,
567
                              enforce_lo_lim);
563
  /*@ensures trans_Saturation((Signal),
564
                              (*s_out),
565
                              (__Saturation_1?\true:\false),
566
                              (__Saturation_2?\true:\false),
567
                              (enforce_lo_lim));
568 568
  assigns *s_out, __Saturation_1, __Saturation_2, enforce_lo_lim;
569 569
  */
570 570
  {
571 571
  
572 572
  /*@
573
  ensures (__Saturation_1 == (0.0001 >= Signal));
573
  ensures ((__Saturation_1?\true:\false) == (0.0001 >= (Signal)));
574 574
  assigns __Saturation_1;
575 575
  */
576 576
  {
577 577
  __Saturation_1 = (0.0001 >= Signal);
578 578
  }
579 579
  /*@
580
  ensures (enforce_lo_lim == (__Saturation_1?(0.0001):(Signal)));
580
  ensures ((enforce_lo_lim) == ((__Saturation_1?\true:\false)?(0.0001):((Signal))));
581 581
  assigns enforce_lo_lim;
582 582
  */
583 583
  {
584 584
  enforce_lo_lim = (__Saturation_1?(0.0001):(Signal));
585 585
  }
586 586
  /*@
587
  ensures (__Saturation_2 == (1000. <= enforce_lo_lim));
587
  ensures ((__Saturation_2?\true:\false) == (1000. <= (enforce_lo_lim)));
588 588
  assigns __Saturation_2;
589 589
  */
590 590
  {
591 591
  __Saturation_2 = (1000. <= enforce_lo_lim);
592 592
  }
593 593
  /*@
594
  ensures (*s_out == (__Saturation_2?(1000.):(enforce_lo_lim)));
594
  ensures ((*s_out) == ((__Saturation_2?\true:\false)?(1000.):((enforce_lo_lim))));
595 595
  assigns *s_out;
596 596
  */
597 597
  {
......
614 614
void integrator_reset_step (double Fx, _Bool ResetLevel, double x0, 
615 615
                            double (*ir_out),
616 616
                            struct integrator_reset_mem *self) {
617
  /*@ensures Ctrans_integrator_reset(Fx,
618
                                     ResetLevel,
619
                                     x0,
620
                                     *ir_out,
617
  /*@ensures Ctrans_integrator_reset((Fx),
618
                                     (ResetLevel?\true:\false),
619
                                     (x0),
620
                                     (*ir_out),
621 621
                                     \at(*self, Pre),
622 622
                                     (*self));
623 623
  assigns *ir_out, *self;
......
628 628
  
629 629
  
630 630
  /* Asserting trans predicate: locals are [] */
631
  /*@ensures trans_integrator_reset(Fx,
632
                                    ResetLevel,
633
                                    x0,
634
                                    *ir_out,
631
  /*@ensures trans_integrator_reset((Fx),
632
                                    (ResetLevel?\true:\false),
633
                                    (x0),
634
                                    (*ir_out),
635 635
                                    \at(*self, Pre),
636 636
                                    (*self),
637
                                    __integrator_reset_1);
637
                                    (__integrator_reset_1?\true:\false));
638 638
  assigns *ir_out, *self, __integrator_reset_1;
639 639
  */
640 640
  {
641 641
  
642 642
  
643 643
  /*@
644
  ensures (__integrator_reset_1==(\at(*self, Pre).ni_3._reg._first?(1):(0))) && ((*self).ni_3._reg._first==0);
644
  ensures ((__integrator_reset_1?\true:\false)==(\at(*self, Pre).ni_3._reg._first?(1):(0))) && ((*self).ni_3._reg._first==0);
645 645
  assigns __integrator_reset_1, (*self).ni_3;
646 646
  */
647 647
  {
648 648
  _arrow_step (1, 0, &__integrator_reset_1, &self->ni_3);
649 649
  }
650 650
  /*@
651
  ensures (*ir_out == (__integrator_reset_1?(x0):((ResetLevel?(x0):(((Fx * 1.) + \at(*self, Pre)._reg.__integrator_reset_2))))));
651
  ensures ((*ir_out) == ((__integrator_reset_1?\true:\false)?((x0)):(((ResetLevel?\true:\false)?((x0)):((((Fx) * 1.) + \at(*self, Pre)._reg.__integrator_reset_2))))));
652 652
  assigns *ir_out;
653 653
  */
654 654
  {
655 655
  *ir_out = (__integrator_reset_1?(x0):((ResetLevel?(x0):(((Fx * 1.) + self->_reg.__integrator_reset_2)))));
656 656
  }
657 657
  /*@
658
  ensures ((*self)._reg.__integrator_reset_2 == *ir_out);
658
  ensures ((*self)._reg.__integrator_reset_2 == (*ir_out));
659 659
  assigns (*self)._reg.__integrator_reset_2;
660 660
  */
661 661
  {
......
668 668
                                   double lo_lim, 
669 669
                                   double (*out)
670 670
                                   ) {
671
  /*@ensures Ctrans_VariableLimitSaturation(up_lim,
672
                                            Signal,
673
                                            lo_lim,
674
                                            *out);
671
  /*@ensures Ctrans_VariableLimitSaturation((up_lim),
672
                                            (Signal),
673
                                            (lo_lim),
674
                                            (*out));
675 675
  assigns *out;
676 676
  */
677 677
  {
......
682 682
  
683 683
  
684 684
  /* Asserting trans predicate: locals are [] */
685
  /*@ensures trans_VariableLimitSaturation(up_lim,
686
                                           Signal,
687
                                           lo_lim,
688
                                           *out,
689
                                           __VariableLimitSaturation_1,
690
                                           __VariableLimitSaturation_2,
691
                                           enforce_lo_lim);
685
  /*@ensures trans_VariableLimitSaturation((up_lim),
686
                                           (Signal),
687
                                           (lo_lim),
688
                                           (*out),
689
                                           (__VariableLimitSaturation_1?\true:\false),
690
                                           (__VariableLimitSaturation_2?\true:\false),
691
                                           (enforce_lo_lim));
692 692
  assigns *out, __VariableLimitSaturation_1, __VariableLimitSaturation_2,
693 693
          enforce_lo_lim;
694 694
  */
695 695
  {
696 696
  
697 697
  /*@
698
  ensures (__VariableLimitSaturation_1 == (Signal >= lo_lim));
698
  ensures ((__VariableLimitSaturation_1?\true:\false) == ((Signal) >= (lo_lim)));
699 699
  assigns __VariableLimitSaturation_1;
700 700
  */
701 701
  {
702 702
  __VariableLimitSaturation_1 = (Signal >= lo_lim);
703 703
  }
704 704
  /*@
705
  ensures (enforce_lo_lim == (__VariableLimitSaturation_1?(Signal):(lo_lim)));
705
  ensures ((enforce_lo_lim) == ((__VariableLimitSaturation_1?\true:\false)?((Signal)):((lo_lim))));
706 706
  assigns enforce_lo_lim;
707 707
  */
708 708
  {
709 709
  enforce_lo_lim = (__VariableLimitSaturation_1?(Signal):(lo_lim));
710 710
  }
711 711
  /*@
712
  ensures (__VariableLimitSaturation_2 == (enforce_lo_lim <= up_lim));
712
  ensures ((__VariableLimitSaturation_2?\true:\false) == ((enforce_lo_lim) <= (up_lim)));
713 713
  assigns __VariableLimitSaturation_2;
714 714
  */
715 715
  {
716 716
  __VariableLimitSaturation_2 = (enforce_lo_lim <= up_lim);
717 717
  }
718 718
  /*@
719
  ensures (*out == (__VariableLimitSaturation_2?(enforce_lo_lim):(up_lim)));
719
  ensures ((*out) == ((__VariableLimitSaturation_2?\true:\false)?((enforce_lo_lim)):((up_lim))));
720 720
  assigns *out;
721 721
  */
722 722
  {

Also available in: Unified diff