Project

General

Profile

« Previous | Next » 

Revision bff13707

Added by Guillaume Davy over 9 years ago

ALT_2 working with modification made by hand

View differences:

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