Revision 97602f7c
Added by Guillaume Davy over 9 years ago
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
Correct bug when there is no precondition and change reprensentation
of boolean in ACSL