Revision bff13707
Added by Guillaume Davy over 10 years ago
| src/backends/C/c_backend_proof.ml | ||
|---|---|---|
| 158 | 158 |
(pp_acsl_val mem1 (pp_acsl_var_read [])) y |
| 159 | 159 |
self i |
| 160 | 160 |
| MStep (il, i, vl) -> |
| 161 |
let pp_val fmt x = (match get_val_type x with Types.Tbool -> fprintf fmt "((%a)?1:0)" | _ -> fprintf fmt "%a") (pp_acsl_val mem1 (pp_acsl_var_read [])) x in
|
|
| 161 |
let pp_val fmt x = (match get_val_type x with Types.Tbool -> fprintf fmt "%a" | _ -> fprintf fmt "%a") (pp_acsl_val mem1 (pp_acsl_var_read [])) x in
|
|
| 162 | 162 |
pp_acsl_fun ("Ctrans_"^(node_name (fst (List.assoc i calls)))) fmt
|
| 163 | 163 |
((List.map (fun x fmt-> fprintf fmt "%a %a" pp_cast (get_val_type x) pp_val x) vl)@ |
| 164 | 164 |
(List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read []) x) il)@ |
| ... | ... | |
| 216 | 216 |
(pp_acsl_at self s) |
| 217 | 217 |
*) |
| 218 | 218 |
|
| 219 |
(* |
|
| 220 |
Require Why3. |
|
| 221 |
intros. |
|
| 222 |
unfold P_trans_AltitudeControl. |
|
| 223 |
repeat split. |
|
| 224 |
why3 "Z3" timelimit 10. |
|
| 225 |
why3 "Z3" timelimit 10. |
|
| 226 |
why3 "Z3" timelimit 10. |
|
| 227 |
why3 "Z3" timelimit 10. |
|
| 228 |
why3 "Z3" timelimit 10. |
|
| 229 |
why3 "Z3" timelimit 10. |
|
| 230 |
why3 "Z3" timelimit 10. |
|
| 231 |
why3 "Z3" timelimit 10. |
|
| 232 |
why3 "Z3" timelimit 10. |
|
| 233 |
why3 "Z3" timelimit 10. |
|
| 234 |
why3 "Z3" timelimit 10. |
|
| 235 |
why3 "Z3" timelimit 10. |
|
| 236 |
why3 "Z3" timelimit 10. |
|
| 237 |
why3 "Z3" timelimit 10. |
|
| 238 |
why3 "Z3" timelimit 10. |
|
| 239 |
why3 "Z3" timelimit 10. |
|
| 240 |
why3 "Z3" timelimit 10. |
|
| 241 |
why3 "Z3" timelimit 10. |
|
| 242 |
assert (a_9 = F_AltitudeControl_mem_ni_1 a_6). |
|
| 243 |
why3 "Z3" timelimit 10. |
|
| 244 |
assert (a_10 = F_AltitudeControl_mem_ni_1 a_7). |
|
| 245 |
unfold F_AltitudeControl_mem_ni_1. |
|
| 246 |
unfold a_7. |
|
| 247 |
unfold Load_S_AltitudeControl_mem. |
|
| 248 |
unfold a_10. |
|
| 249 |
unfold a_8. |
|
| 250 |
unfold havoc in H36. |
|
| 251 |
unfold get. |
|
| 252 |
clear. |
|
| 253 |
rewrite <- H48. |
|
| 254 |
rewrite <- H49. |
|
| 255 |
apply H47. |
|
| 256 |
*) |
|
| 257 |
|
|
| 219 | 258 |
(* Print a transition call/decl in acsl *) |
| 220 | 259 |
let pp_acsl_fun_trans infos pre name inputs outputs suffix flag_output self flag_mem locals fmt existential = |
| 221 | 260 |
let (locals, existential) = (*([], match existential with None -> None | Some x -> Some []) else*) |
| ... | ... | |
| 230 | 269 |
in |
| 231 | 270 |
let mems = function 1 -> "Pre" | 2 -> "Here" | _ -> assert false in |
| 232 | 271 |
let pp_self_read = |
| 233 |
if flag_mem then fun i fmt-> fprintf fmt "\\at(*%s, %s)" self (mems i)
|
|
| 272 |
if flag_mem then fun i fmt-> (match i with 1 -> fprintf fmt "\\at(*%s, Pre)" self | 2 -> fprintf fmt "(*%s)" self | _ -> assert false)
|
|
| 234 | 273 |
else fun i fmt-> fprintf fmt "%s%i" self (match suffix with None -> i | Some s -> s+i-1) |
| 235 | 274 |
in |
| 236 | 275 |
let (pp_var, pp_self) = |
| tcm_benchmarks/ALT2/ALT2_proof/ALT_2.lustrec.c | ||
|---|---|---|
| 27 | 27 |
hdotChgRate, |
| 28 | 28 |
*obs, |
| 29 | 29 |
\at(*self, Pre), |
| 30 |
\at(*self, Here));
|
|
| 30 |
(*self));
|
|
| 31 | 31 |
assigns *obs, *self; |
| 32 | 32 |
*/ |
| 33 | 33 |
{
|
| ... | ... | |
| 46 | 46 |
hdotChgRate, |
| 47 | 47 |
*obs, |
| 48 | 48 |
\at(*self, Pre), |
| 49 |
\at(*self, Here),
|
|
| 49 |
(*self),
|
|
| 50 | 50 |
altgammaCmd, |
| 51 | 51 |
tempAlt); |
| 52 | 52 |
assigns *obs, *self, altgammaCmd, tempAlt; |
| ... | ... | |
| 61 | 61 |
hdotChgRate, |
| 62 | 62 |
*obs, |
| 63 | 63 |
\at(*self, Pre), |
| 64 |
\at(*self, Here),
|
|
| 64 |
(*self),
|
|
| 65 | 65 |
altgammaCmd, |
| 66 | 66 |
tempAlt); |
| 67 | 67 |
assigns *obs, *self, altgammaCmd, tempAlt; |
| ... | ... | |
| 105 | 105 |
hdotChgRate_Out1_69, |
| 106 | 106 |
*altgammacmd_In1_661, |
| 107 | 107 |
\at(*self, Pre), |
| 108 |
\at(*self, Here));
|
|
| 108 |
(*self));
|
|
| 109 | 109 |
assigns *altgammacmd_In1_661, *self; |
| 110 | 110 |
*/ |
| 111 | 111 |
{
|
| ... | ... | |
| 142 | 142 |
hdotChgRate_Out1_69, |
| 143 | 143 |
*altgammacmd_In1_661, |
| 144 | 144 |
\at(*self, Pre), |
| 145 |
\at(*self, Here),
|
|
| 145 |
(*self),
|
|
| 146 | 146 |
Abs_Out1_144, |
| 147 | 147 |
Kh_Out1_193, |
| 148 | 148 |
Logical_Operator_In1_197, |
| ... | ... | |
| 181 | 181 |
hdotChgRate_Out1_69, |
| 182 | 182 |
*altgammacmd_In1_661, |
| 183 | 183 |
\at(*self, Pre), |
| 184 |
\at(*self, Here),
|
|
| 184 |
(*self),
|
|
| 185 | 185 |
Abs_Out1_144, |
| 186 | 186 |
Kh_Out1_193, |
| 187 | 187 |
Logical_Operator_In1_197, |
| ... | ... | |
| 219 | 219 |
hdotChgRate_Out1_69, |
| 220 | 220 |
*altgammacmd_In1_661, |
| 221 | 221 |
\at(*self, Pre), |
| 222 |
\at(*self, Here),
|
|
| 222 |
(*self),
|
|
| 223 | 223 |
Abs_Out1_144, |
| 224 | 224 |
Kh_Out1_193, |
| 225 | 225 |
Logical_Operator_In1_197, |
| ... | ... | |
| 256 | 256 |
hdotChgRate_Out1_69, |
| 257 | 257 |
*altgammacmd_In1_661, |
| 258 | 258 |
\at(*self, Pre), |
| 259 |
\at(*self, Here),
|
|
| 259 |
(*self),
|
|
| 260 | 260 |
Abs_Out1_144, |
| 261 | 261 |
Kh_Out1_193, |
| 262 | 262 |
Logical_Operator_In1_197, |
| ... | ... | |
| 333 | 333 |
Sum_Out1_286 = (AltCmd_Out1_29 + (- Alt_Out1_39)); |
| 334 | 334 |
Kh_Out1_193 = (0.08 * Sum_Out1_286); |
| 335 | 335 |
Switch_Out1_305 = (Switch_In2_303?(Kh_Out1_193):(0.)); |
| 336 |
/*@ |
|
| 337 |
ensures Ctrans_VariableLimitSaturation((double) Sum3_Out1_296, |
|
| 338 |
(double) Switch_Out1_305, |
|
| 339 |
(double) k_Out1_585, |
|
| 340 |
Variable_Limit_Saturation_0_Out1_509); |
|
| 341 |
assigns Variable_Limit_Saturation_0_Out1_509; |
|
| 342 |
*/ {
|
|
| 336 | 343 |
VariableLimitSaturation_step (Sum3_Out1_296, Switch_Out1_305, k_Out1_585, &Variable_Limit_Saturation_0_Out1_509); |
| 344 |
} |
|
| 345 |
/*@ |
|
| 346 |
ensures Ctrans_VariableRateLimit((double) hdotChgRate_Out1_69, |
|
| 347 |
(double) Variable_Limit_Saturation_0_Out1_509, |
|
| 348 |
(_Bool) ((Logical_Operator_Out1_198)?1:0), |
|
| 349 |
(double) hdot_Out1_59, |
|
| 350 |
Variable__Rate_Limit_Out1_324, |
|
| 351 |
\at(*self, Pre).ni_1, |
|
| 352 |
(*self).ni_1); |
|
| 353 |
assigns Variable__Rate_Limit_Out1_324, self->ni_1; |
|
| 354 |
*/ {
|
|
| 337 | 355 |
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_1); |
| 356 |
} |
|
| 338 | 357 |
r2d_Out1_603 = (57.2958 * Variable__Rate_Limit_Out1_324); |
| 339 | 358 |
kts2fps_Out1_594 = (1.6878 * GsKts_Out1_49); |
| 340 | 359 |
Switch1_In2_312 = (__AltitudeControl_2?(0):(1)); |
| ... | ... | |
| 360 | 379 |
IC_Out1_364, |
| 361 | 380 |
*output_In1_489, |
| 362 | 381 |
\at(*self, Pre), |
| 363 |
\at(*self, Here));
|
|
| 382 |
(*self));
|
|
| 364 | 383 |
assigns *output_In1_489, *self; |
| 365 | 384 |
*/ |
| 366 | 385 |
{
|
| ... | ... | |
| 383 | 402 |
IC_Out1_364, |
| 384 | 403 |
*output_In1_489, |
| 385 | 404 |
\at(*self, Pre), |
| 386 |
\at(*self, Here),
|
|
| 405 |
(*self),
|
|
| 387 | 406 |
Gain1_Out1_382, |
| 388 | 407 |
Gain_Out1_373, |
| 389 | 408 |
Integrator1_Out1_391, |
| ... | ... | |
| 405 | 424 |
IC_Out1_364, |
| 406 | 425 |
*output_In1_489, |
| 407 | 426 |
\at(*self, Pre), |
| 408 |
\at(*self, Here),
|
|
| 427 |
(*self),
|
|
| 409 | 428 |
Gain1_Out1_382, |
| 410 | 429 |
Gain_Out1_373, |
| 411 | 430 |
Integrator1_Out1_391, |
| ... | ... | |
| 426 | 445 |
IC_Out1_364, |
| 427 | 446 |
*output_In1_489, |
| 428 | 447 |
\at(*self, Pre), |
| 429 |
\at(*self, Here),
|
|
| 448 |
(*self),
|
|
| 430 | 449 |
Gain1_Out1_382, |
| 431 | 450 |
Gain_Out1_373, |
| 432 | 451 |
Integrator1_Out1_391, |
| ... | ... | |
| 440 | 459 |
__VariableRateLimit_2; |
| 441 | 460 |
*/ |
| 442 | 461 |
{
|
| 443 |
/*@ ensures (__VariableRateLimit_1==(\at(*self, Pre).ni_3._reg._first?(1):(0))) && ((*self).ni_3._reg._first==0); |
|
| 462 |
/*@ ensures (__VariableRateLimit_1==(\at(*self, Pre).ni_3._reg._first?(1):(0))); |
|
| 463 |
ensures ((*self).ni_3._reg._first==0); |
|
| 444 | 464 |
ensures (Integrator1_Out1_391 == (__VariableRateLimit_1?(IC_Out1_364):(\at(*self, Pre)._reg.__VariableRateLimit_3))); |
| 445 | 465 |
ensures (*output_In1_489 == Integrator1_Out1_391); |
| 446 | 466 |
ensures (Gain1_Out1_382 == (- ratelim_Out1_334)); |
| ... | ... | |
| 451 | 471 |
(double) Gain1_Out1_382, |
| 452 | 472 |
Variable_Limit_Saturation_Out1_410); |
| 453 | 473 |
ensures Ctrans_integrator_reset((double) Variable_Limit_Saturation_Out1_410, |
| 454 |
(_Bool) ((ICtrig_Out1_354)?1:0),
|
|
| 474 |
ICtrig_Out1_354,
|
|
| 455 | 475 |
(double) IC_Out1_364, |
| 456 | 476 |
__VariableRateLimit_2, |
| 457 | 477 |
\at(*self, Pre).ni_2, |
| ... | ... | |
| 465 | 485 |
|
| 466 | 486 |
_arrow_step (1, 0, &__VariableRateLimit_1, &self->ni_3); |
| 467 | 487 |
Integrator1_Out1_391 = (__VariableRateLimit_1?(IC_Out1_364):(self->_reg.__VariableRateLimit_3)); |
| 488 |
/*@ |
|
| 489 |
ensures (*output_In1_489 == Integrator1_Out1_391); |
|
| 490 |
assigns *output_In1_489; */ |
|
| 491 |
{
|
|
| 468 | 492 |
*output_In1_489 = Integrator1_Out1_391; |
| 493 |
} |
|
| 469 | 494 |
Gain1_Out1_382 = (- ratelim_Out1_334); |
| 470 | 495 |
Sum2_Out1_401 = (input_Out1_344 + (- Integrator1_Out1_391)); |
| 471 | 496 |
Gain_Out1_373 = (20. * Sum2_Out1_401); |
| 497 |
/*@ |
|
| 498 |
ensures Ctrans_VariableLimitSaturation((double) ratelim_Out1_334, |
|
| 499 |
(double) Gain_Out1_373, |
|
| 500 |
(double) Gain1_Out1_382, |
|
| 501 |
Variable_Limit_Saturation_Out1_410); |
|
| 502 |
assigns Variable_Limit_Saturation_Out1_410; */ |
|
| 503 |
{
|
|
| 472 | 504 |
VariableLimitSaturation_step (ratelim_Out1_334, Gain_Out1_373, Gain1_Out1_382, &Variable_Limit_Saturation_Out1_410); |
| 505 |
} |
|
| 506 |
/*@ |
|
| 507 |
ensures Ctrans_integrator_reset((double) Variable_Limit_Saturation_Out1_410, |
|
| 508 |
(_Bool) ((ICtrig_Out1_354)), |
|
| 509 |
(double) IC_Out1_364, |
|
| 510 |
__VariableRateLimit_2, |
|
| 511 |
\at(*self, Pre).ni_2, |
|
| 512 |
(*self).ni_2); |
|
| 513 |
assigns __VariableRateLimit_2, self->ni_2; */ |
|
| 514 |
{
|
|
| 473 | 515 |
integrator_reset_step (Variable_Limit_Saturation_Out1_410, ICtrig_Out1_354, IC_Out1_364, &__VariableRateLimit_2, &self->ni_2); |
| 516 |
} |
|
| 474 | 517 |
self->_reg.__VariableRateLimit_3 = __VariableRateLimit_2; |
| 475 | 518 |
}}}}}return; |
| 476 | 519 |
} |
| ... | ... | |
| 524 | 567 |
x0, |
| 525 | 568 |
*ir_out, |
| 526 | 569 |
\at(*self, Pre), |
| 527 |
\at(*self, Here));
|
|
| 570 |
(*self));
|
|
| 528 | 571 |
assigns *ir_out, *self; |
| 529 | 572 |
*/ |
| 530 | 573 |
{
|
| ... | ... | |
| 538 | 581 |
x0, |
| 539 | 582 |
*ir_out, |
| 540 | 583 |
\at(*self, Pre), |
| 541 |
\at(*self, Here),
|
|
| 584 |
(*self),
|
|
| 542 | 585 |
__integrator_reset_1); |
| 543 | 586 |
assigns *ir_out, *self, __integrator_reset_1; |
| 544 | 587 |
*/ |
| tcm_benchmarks/ALT2/ALT2_proof/ALT_2.lustrec.h | ||
|---|---|---|
| 114 | 114 |
x0, |
| 115 | 115 |
*ir_out, |
| 116 | 116 |
\at(*self, Pre), |
| 117 |
\at(*self, Here));
|
|
| 117 |
(*self));
|
|
| 118 | 118 |
assigns *ir_out, *self; |
| 119 | 119 |
*/ |
| 120 | 120 |
extern void integrator_reset_step (double Fx, _Bool ResetLevel, double x0, |
| ... | ... | |
| 178 | 178 |
(double) Gain1_Out1_382, |
| 179 | 179 |
Variable_Limit_Saturation_Out1_410) && |
| 180 | 180 |
Ctrans_integrator_reset((double) Variable_Limit_Saturation_Out1_410, |
| 181 |
(_Bool) ((ICtrig_Out1_354)?1:0),
|
|
| 181 |
ICtrig_Out1_354,
|
|
| 182 | 182 |
(double) IC_Out1_364, |
| 183 | 183 |
__VariableRateLimit_2, |
| 184 | 184 |
self1.ni_2, |
| ... | ... | |
| 243 | 243 |
IC_Out1_364, |
| 244 | 244 |
*output_In1_489, |
| 245 | 245 |
\at(*self, Pre), |
| 246 |
\at(*self, Here));
|
|
| 246 |
(*self));
|
|
| 247 | 247 |
assigns *output_In1_489, *self; |
| 248 | 248 |
*/ |
| 249 | 249 |
extern void VariableRateLimit_step (double ratelim_Out1_334, |
| ... | ... | |
| 579 | 579 |
hdotChgRate_Out1_69, |
| 580 | 580 |
*altgammacmd_In1_661, |
| 581 | 581 |
\at(*self, Pre), |
| 582 |
\at(*self, Here));
|
|
| 582 |
(*self));
|
|
| 583 | 583 |
|
| 584 | 584 |
assigns *altgammacmd_In1_661, *self; |
| 585 | 585 |
|
| ... | ... | |
| 667 | 667 |
hdotChgRate, |
| 668 | 668 |
*obs, |
| 669 | 669 |
\at(*self, Pre), |
| 670 |
\at(*self, Here));
|
|
| 670 |
(*self));
|
|
| 671 | 671 |
assigns *obs, *self; |
| 672 | 672 |
*/ |
| 673 | 673 |
extern void top_step (_Bool AltEng, double AltCmd, double Altitude, |
Also available in: Unified diff
ALT_2 working with modification made by hand