Project

General

Profile

« Previous | Next » 

Revision 97602f7c

Added by Guillaume Davy over 10 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