Project

General

Profile

« Previous | Next » 

Revision 97602f7c

Added by Guillaume Davy over 9 years ago

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

View differences:

src/backends/C/c_backend_proof.ml
88 88
        pp_acsl_fun_init (node_name node) self i fmt (Some "")
89 89
    | MLocalAssign (i,v) -> 
90 90
      (match i.var_type.tdesc with Tbool -> fprintf fmt "((!%a) == (!%a))" | _ -> fprintf fmt "(%a == %a)")
91
      (pp_acsl_var_read pointer) i
92
      (pp_acsl_val mem1 (pp_acsl_var_read pointer)) v
91
      (pp_acsl_var_read "" pointer) i
92
      (pp_acsl_val mem1 (pp_acsl_var_read "" pointer)) v
93 93
    | MStateAssign (i,v) ->
94 94
      (match i.var_type.tdesc with Tbool -> fprintf fmt "((!%a) == (!%a))" | _ -> fprintf fmt "(%a == %a)")
95
      (pp_acsl_val mem2 (pp_acsl_var_read pointer)) (StateVar i)
96
      (pp_acsl_val mem1 (pp_acsl_var_read pointer)) v
95
      (pp_acsl_val mem2 (fun fmt v-> fprintf fmt "%s" v.var_id)) (StateVar i)
96
      (pp_acsl_val mem1 (pp_acsl_var_read "" pointer)) v
97 97
    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
98 98
      pp_acsl_instr init vars calls instances self pointer fmt (MLocalAssign (i0, Fun (i, vl)))
99 99
    | MStep ([i0], i, [x;y]) when (not (Basic_library.is_internal_fun i)) && (node_name (fst (List.assoc i calls)) = "_arrow") ->
100 100
      fprintf fmt "(%a==(%s1.%s._reg._first?(%a):(%a))) && (%s2.%s._reg._first==0)"
101
        (pp_acsl_var_read pointer) i0
101
        (pp_acsl_var_read "" pointer) i0
102 102
        self i
103
        (pp_acsl_val mem1 (pp_acsl_var_read [])) x
104
        (pp_acsl_val mem1 (pp_acsl_var_read [])) y
103
        (pp_acsl_val mem1 (pp_acsl_var_read "" [])) x
104
        (pp_acsl_val mem1 (pp_acsl_var_read "" [])) y
105 105
        self i
106 106
    | MStep (il, i, vl) ->
107
      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
107
      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
108 108
      pp_acsl_fun ("Ctrans_"^(node_name (fst (List.assoc i calls)))) fmt
109
      ((List.map (fun x fmt-> fprintf fmt "%a %a" pp_cast (get_val_type x) pp_val x) vl)@
110
      (List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read []) x) il)@
109
      ((List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_val_type x)*) pp_val x) vl)@
110
      (List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read "" []) x) il)@
111 111
        (try ignore(List.assoc i instances);[(fun fmt->fprintf fmt "%s1.%s" self i);(fun fmt->fprintf fmt "%s2.%s" self i)] with Not_found -> []))
112 112
    | MBranch (g,hl) -> assert false (*TODO: useless : ????
113 113
      let t = fst (List.hd hl) in
......
134 134
    match v with
135 135
      | Fun (s, [x;y]) when String.length s >= 6 && String.sub s 0 6 = "arrow_" ->
136 136
        let var = String.sub s 6 (String.length s - 6) in
137
        fprintf fmt "\\let %a = %s1.%s._reg._first?%a:%a; (%s2.%s._reg._first==0) &&"
138
          (pp_acsl_var_read pointer) i
137
        fprintf fmt "\\let %s = %s1.%s._reg._first?%a:%a; (%s2.%s._reg._first==0) &&"
138
          i.var_id
139 139
          self var
140
          (pp_acsl_val (self^"1") (pp_acsl_var_read [])) x
141
          (pp_acsl_val (self^"1") (pp_acsl_var_read [])) y
140
          (pp_acsl_val (self^"1") (pp_acsl_var_read "" [])) x
141
          (pp_acsl_val (self^"1") (pp_acsl_var_read "" [])) y
142 142
          self var
143 143
      | _ ->
144
        fprintf fmt "\\let %a = %a;"
145
          (pp_acsl_var_read pointer) i
146
          (pp_acsl_val (self^"1") (pp_acsl_var_read pointer)) v
144
        fprintf fmt "\\let %s = %a;"
145
          i.var_id
146
          (pp_acsl_val (self^"1") (pp_acsl_var_read "" pointer)) v
147 147
  in
148 148
  let (locals, instrs) = if fullExists () then ([], instrs) else List.fold_left handle ([], []) instrs in
149 149
  fprintf fmt "%a@,%a"
......
220 220
  in
221 221
  let (pp_var, pp_self) =
222 222
    match existential with
223
      | None    -> (pp_acsl_var_decl, (fun i fmt-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i))
223
      | None    -> ((fun i -> pp_acsl_var_decl), (fun i fmt-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i))
224 224
      | Some ex -> (if List.length ex != 0 then fprintf fmt "\\exists %a;@," (Utils.fprintf_list ~sep:";@,\\exists " pp_acsl_var_decl) ex);
225
                   (pp_acsl_var_read (if flag_output then outputs else []), pp_self_read)
225
                   ((fun i -> pp_acsl_var_read i (if flag_output then outputs else [])), pp_self_read)
226 226
  in
227
  let pp_vars = List.map (fun x fmt-> match suffix with None-> pp_var fmt x | Some i -> fprintf fmt "%a%i" pp_var x (i+1)) in
227
  let pp_vars = List.map (fun x fmt-> match suffix with None-> pp_var "" fmt x | Some i -> fprintf fmt "%a" (pp_var (string_of_int (i+1))) x) in
228 228
    (pp_acsl_fun (pre^"trans_"^name)) fmt
229 229
    ((pp_vars (inputs@outputs))@(if not (self = "") then [pp_self 1;pp_self 2] else [])@(pp_vars locals))
230 230

  
......
252 252
    fprintf fmt "%a" (pp_acsl_fun_trans  None "C" name inputs outputs (Some i) false self false []) (Some [])
253 253
  in
254 254
  let pp_eexpr_expr self i j fmt ee = 
255
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (fun fmt x-> fprintf fmt "%a%i" (pp_acsl_var_read []) x j)) ee.mmstep_logic.step_inputs self i
255
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read (string_of_int j) [])) ee.mmstep_logic.step_inputs self i
256 256
  in
257 257
  let spec_pred cor preds fmt i =
258 258
    let j = if cor then i + 1 else i in
259
    fprintf fmt "(%a)" (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self i j)) preds
259
    if List.length preds != 0 then
260
        fprintf fmt "(%a)%s" (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self i j)) preds (if cor then " &&@," else "")
261
    else ()
260 262
  in
261 263
  let aux fmt base =
262 264
    let selfs = iter base self (depth-1) in
263 265
    let ios = iterList (base + 1) (inputs@outputs) in
264 266
    (if List.length selfs == 0 && List.length ios == 0 then 
265
      fprintf fmt "(%a%t%a%t%t)"
267
      fprintf fmt "(%a%t%a%t)"
266 268
     else
267
      fprintf fmt "(\\exists %a%t%a;@,%a%t%a%t%t)"
269
      fprintf fmt "(\\exists %a%t%a;@,%a%t%a%t)"
268 270
        (Utils.fprintf_list ~sep:", "   (fun fmt (i, x)-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i)) selfs
269 271
        (Utils.pp_final_char_if_non_empty ", " (iter base self (depth-1)))
270 272
        (Utils.fprintf_list ~sep:", "   (fun fmt (i, x)-> fprintf fmt "%a%i" pp_acsl_var_decl x i)) ios
271 273
    )
272 274
      (Utils.fprintf_list ~sep:"&&@," (fun fmt (i, f)-> fprintf fmt "%a" f i)) (iter base trans_pred (depth-1))
273 275
      (Utils.pp_final_char_if_non_empty "&&@," (iter base trans_pred (depth-1))) 
274
      (Utils.fprintf_list ~sep:"&&@," (fun fmt (i, f)-> fprintf fmt "%a" f i)) (iter base (spec_pred true spec.m_requires) (depth-1))
275
      (Utils.pp_final_char_if_non_empty "&&@," (iter base (spec_pred true spec.m_requires) (depth-1))) 
276
      (Utils.fprintf_list ~sep:"" (fun fmt (i, f)-> fprintf fmt "%a" f i)) (iter base (spec_pred true spec.m_requires) (depth-1))
276 277
      (fun fmt->
277 278
        if base == 0 then
278 279
          Utils.fprintf_list ~sep:"&&@," (fun fmt (i, f)-> fprintf fmt "%a" f i) fmt (iter (base+1) (spec_pred false spec.m_ensures) depth)
......
285 286
(* Print the invariant lemma *)
286 287
let pp_acsl_lem_inv depth name inputs outputs self fmt spec =
287 288
  let pp_eexpr_expr self j fmt ee =
288
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [])) ee.mmstep_logic.step_inputs self j
289
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read "" [])) ee.mmstep_logic.step_inputs self j
289 290
  in
290 291
  fprintf fmt "\\forall %a %s1, %s2, %a;@,%a==>@,%a==>@,%a%t%a"
291 292
    pp_machine_memtype_name name self self
......
311 312
  in
312 313
  let spec_pred fmt i =
313 314
    let pp_eexpr_expr self j fmt ee = 
314
      fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (fun fmt x-> fprintf fmt "%a%i" (pp_acsl_var_read []) x i)) ee.mmstep_logic.step_inputs self j
315
      fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read (string_of_int i) [])) ee.mmstep_logic.step_inputs self j
315 316
    in
316
    fprintf fmt "%a%t(%a)"
317
    (Utils.fprintf_list ~sep:"==>@," ((fun fmt (w, x)-> fprintf fmt "%a"
317
    fprintf fmt "%a(%a)"
318
    (Utils.fprintf_list ~sep:"" ((fun fmt (w, x)-> fprintf fmt "%a%t"
318 319
      (Utils.fprintf_list ~sep:"==>@," (pp_eexpr_expr self (w))) spec.m_requires
320
      (Utils.pp_final_char_if_non_empty "==>@," spec.m_requires)
319 321
    ))) (iter k None (depth -1))
320
    (Utils.pp_final_char_if_non_empty "==>@," spec.m_requires)
321 322
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self (i))) spec.m_ensures
322 323
  in
323 324
  let aux fmt base =
......
342 343
(* Print the spec lemma *)
343 344
let pp_acsl_lem_spec depth name inputs outputs self fmt spec =
344 345
  let pp_eexpr_expr self j fmt ee =
345
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [])) ee.mmstep_logic.step_inputs self j
346
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read "" [])) ee.mmstep_logic.step_inputs self j
346 347
  in
347 348
  fprintf fmt "\\forall %a %s1, %s2, %a;@,%a==>@,%a==>@,%a%t%a"
348 349
    pp_machine_memtype_name name self self
......
556 557
            pp_acsl_fun_init (node_name node) mem2 i fmt (Some "")
557 558
        | MLocalAssign (i,v) -> 
558 559
          (match i.var_type.tdesc with Tbool -> fprintf fmt "((!%a) == (!%a))" | _ -> fprintf fmt "(%a == %a)")
559
          (pp_acsl_var_read pointer) i
560
          (pp_acsl_val mem1 (pp_acsl_var_read pointer)) v
560
          (pp_acsl_var_read "" pointer) i
561
          (pp_acsl_val mem1 (pp_acsl_var_read "" pointer)) v
561 562
        | MStateAssign (i,v) ->
562 563
          (match i.var_type.tdesc with Tbool -> fprintf fmt "((!%a) == (!%a))" | _ -> fprintf fmt "(%a == %a)")
563
          (pp_acsl_val mem2 (pp_acsl_var_read pointer)) (StateVar i)
564
          (pp_acsl_val mem1 (pp_acsl_var_read pointer)) v
564
          (pp_acsl_val mem2 (pp_acsl_var_read "" pointer)) (StateVar i)
565
          (pp_acsl_val mem1 (pp_acsl_var_read "" pointer)) v
565 566
        | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
566 567
          pp_instr fmt (MLocalAssign (i0, Fun (i, vl)))
567 568
        | MStep ([i0], i, [x;y]) when (not (Basic_library.is_internal_fun i)) && (node_name (fst (List.assoc i m.mcalls)) = "_arrow") ->
568 569
          fprintf fmt "(%a==(%s.%s._reg._first?(%a):(%a))) && (%s.%s._reg._first==0)"
569
            (pp_acsl_var_read pointer) i0
570
            (pp_acsl_var_read "" pointer) i0
570 571
            mem1 i
571
            (pp_acsl_val mem1 (pp_acsl_var_read [])) x
572
            (pp_acsl_val mem1 (pp_acsl_var_read [])) y
572
            (pp_acsl_val mem1 (pp_acsl_var_read "" [])) x
573
            (pp_acsl_val mem1 (pp_acsl_var_read "" [])) y
573 574
            mem2 i
574 575
        | MStep (il, i, vl) ->
575
          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
576
          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
576 577
          pp_acsl_fun ("Ctrans_"^(node_name (fst (List.assoc i m.mcalls)))) fmt
577
          ((List.map (fun x fmt-> fprintf fmt "%a %a" pp_cast (get_val_type x) pp_val x) vl)@
578
          (List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read []) x) il)@
578
          ((List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_val_type x)*) pp_val x) vl)@
579
          (List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read "" []) x) il)@
579 580
            (try ignore(List.assoc i m.minstances);[(fun fmt->fprintf fmt "%s.%s" mem1 i);(fun fmt->fprintf fmt "%s.%s" mem2 i)] with Not_found -> []))
580 581
        | MBranch (g,hl) -> assert false
581 582
      in
582 583
      let mods = match instr with
583 584
        | MReset i -> [fun fmt -> fprintf fmt "%s.%s" mem2 i]
584
        | MLocalAssign (i,v) -> [fun fmt -> fprintf fmt "%a" (pp_acsl_var_read pointer) i]
585
        | MStateAssign (i,v) -> [fun fmt -> fprintf fmt "%a" (pp_acsl_val mem2 (pp_acsl_var_read pointer)) (StateVar i)]
586
        | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> [fun fmt -> fprintf fmt "%a" (pp_acsl_var_read pointer) i0]
585
        | MLocalAssign (i,v) -> [fun fmt -> if List.exists (fun o -> o.var_id = i.var_id) pointer
586
    then fprintf fmt "*%s" i.var_id
587
    else fprintf fmt "%s" i.var_id]
588
        | MStateAssign (i,v) -> [fun fmt -> fprintf fmt "%a" (pp_acsl_val mem2 (pp_acsl_var_read "" pointer)) (StateVar i)]
589
        | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> [fun fmt -> fprintf fmt "%a" (pp_acsl_var_read "" pointer) i0]
587 590
        | MStep ([i0], i, [x;y]) when (not (Basic_library.is_internal_fun i)) && (node_name (fst (List.assoc i m.mcalls)) = "_arrow") ->
588
          [fun fmt-> fprintf fmt "%a, %s.%s" (pp_acsl_var_read pointer) i0 mem2 i]
589
        | MStep (il, i, vl) -> (List.map (fun x fmt-> fprintf fmt "%a" (pp_acsl_var_read []) x) il)@
591
          [fun fmt-> fprintf fmt "%t, %s.%s" (fun fmt -> if List.exists (fun o -> o.var_id = i0.var_id) pointer
592
    then fprintf fmt "*%s" i0.var_id
593
    else fprintf fmt "%s" i0.var_id) mem2 i]
594
        | MStep (il, i, vl) -> (List.map (fun x fmt-> if List.exists (fun o -> o.var_id = x.var_id) pointer
595
    then fprintf fmt "*%s" x.var_id
596
    else fprintf fmt "%s" x.var_id) il)@
590 597
            (try ignore(List.assoc i m.minstances);[(fun fmt->fprintf fmt "%s.%s" mem1 i);(fun fmt->fprintf fmt "%s.%s" mem2 i)] with Not_found -> [])
591 598
        | MBranch (g,hl) -> assert false
592 599
      in
src/backends/C/c_backend_spec.ml
72 72
  let rec aux t pp_suffix =
73 73
  match (Types.repr t).Types.tdesc with
74 74
  | Types.Tclock t'       -> aux t' pp_suffix
75
  | Types.Tbool           -> fprintf fmt "integer %s%a" var pp_suffix ()
75
  | Types.Tbool           -> fprintf fmt "boolean %s%a" var pp_suffix ()
76 76
  | Types.Treal           -> fprintf fmt "real %s%a" var pp_suffix ()
77 77
  | Types.Tint            -> fprintf fmt "integer %s%a" var pp_suffix ()
78 78
  | Types.Tarray (d, t')  ->
......
365 365
    | StateVar v    ->     
366 366
      if Types.is_array_type v.var_type
367 367
      then assert false
368
      else fprintf fmt "%s%s_reg.%a" self 
369
     (if !Options.no_pointer then "." else "->") pp_var v
368
      else fprintf fmt "%s%s_reg.%s" self 
369
     (if !Options.no_pointer then "." else "->") v.var_id
370 370
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (basic_lib_pp_acsl n Machine_code.get_val_type (pp_acsl_val self pp_var)) vl
371 371
      
372 372

  
......
440 440
     despite its scalar Lustre type)
441 441
   - moreover, cast arrays variables into their original array type.
442 442
*)
443
let pp_acsl_var_read outputs fmt id =
443
let pp_acsl_var_read suffix outputs fmt id =
444 444
  if Types.is_array_type id.var_type
445 445
  then
446 446
    assert false (* no array *)
447 447
  else (
448
    if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)
449
    then fprintf fmt "*%s" id.var_id
450
    else fprintf fmt "%s" id.var_id
448
    (if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)
449
    then fprintf fmt "(*%s%s" id.var_id suffix
450
    else fprintf fmt "(%s%s" id.var_id suffix);
451
      match (Types.repr id.var_type).Types.tdesc with
452
      | Types.Tbool           -> fprintf fmt "?\\true:\\false)"
453
      | _ -> fprintf fmt ")"
451 454
  )
452 455

  
453 456
    
......
548 551
	)
549 552
    | _ -> fprintf fmt "spec_%i(%a%t);" 
550 553
      ee.muid   
551
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read outputs)) ee.mmstep_logic.step_inputs
554
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read "" outputs)) ee.mmstep_logic.step_inputs
552 555
      (fun fmt -> if stateless then fprintf fmt "" else fprintf fmt ", %s%s" (if !Options.no_pointer then "*" else "") self)
553 556
  in
554 557
  fprintf fmt "@[<v 2>/*@@ ";
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
  {
tcm_benchmarks/ALT2/ALT2_proof/ALT_2.lustrec.coq
208 208
eassumption.
209 209
Qed.
210 210

  
211
Goal typed_ref_AltitudeControl_step_stmt_post_5.
211
Goal typed_ref_AltitudeControl_step_stmt_post.
212 212
Hint AltitudeControl_step,default,property.
213 213
Proof.
214
  Require Why3. intros. hnf. repeat split;try why3 "CVC3" timelimit 10;try why3 "Z3" timelimit 10;why3 "CVC4" timelimit 10.
214
(* Require Why3. intros. hnf. repeat split;try why3 "CVC3" timelimit 10;try why3 "Z3" timelimit 10;why3 "CVC4" timelimit 10. *)
215 215
Qed.
216 216

  
217
Goal typed_ref_VariableRateLimit_step_stmt_post.
217
Goal typed_ref_VariableRateLimit_step_stmt_post_4.
218 218
Hint VariableRateLimit_step,default,property.
219 219
Proof.
220 220
(* Require Why3. intros. hnf. repeat split;try why3 "CVC3" timelimit 10;try why3 "Z3" timelimit 10;why3 "CVC4" timelimit 10. *)
221 221
Qed.
222 222

  
223
Goal typed_ref_integrator_reset_step_stmt_post_2.
224
Hint default,integrator_reset_step,property.
225
Proof.
226
  Require Why3. intros. hnf. repeat split;try why3 "CVC3" timelimit 10;try why3 "Z3" timelimit 10;why3 "CVC4" timelimit 10.
227
Qed.
228

  
229 223

  
tcm_benchmarks/ALT2/ALT2_proof/ALT_2.lustrec.h
24 24
                                            real Signal,
25 25
                                            real lo_lim,
26 26
                                            real out,
27
                                            integer __VariableLimitSaturation_1,
28
                                            integer __VariableLimitSaturation_2,
27
                                            boolean __VariableLimitSaturation_1,
28
                                            boolean __VariableLimitSaturation_2,
29 29
                                            real enforce_lo_lim) =
30 30
       
31
       (__VariableLimitSaturation_1 == (Signal >= lo_lim)) &&
32
       (enforce_lo_lim == (__VariableLimitSaturation_1?(Signal):(lo_lim))) &&
33
       (__VariableLimitSaturation_2 == (enforce_lo_lim <= up_lim)) &&
34
       (out == (__VariableLimitSaturation_2?(enforce_lo_lim):(up_lim)));
31
       ((__VariableLimitSaturation_1?\true:\false) == ((Signal) >= (lo_lim))) &&
32
       ((enforce_lo_lim) == ((__VariableLimitSaturation_1?\true:\false)?((Signal)):((lo_lim)))) &&
33
       ((__VariableLimitSaturation_2?\true:\false) == ((enforce_lo_lim) <= (up_lim))) &&
34
       ((out) == ((__VariableLimitSaturation_2?\true:\false)?((enforce_lo_lim)):((up_lim))));
35 35
*/
36 36
/*@ predicate Ctrans_VariableLimitSaturation(real up_lim,
37 37
                                             real Signal,
38 38
                                             real lo_lim,
39 39
                                             real out) =
40
       \exists integer __VariableLimitSaturation_1;
41
       \exists integer __VariableLimitSaturation_2;
40
       \exists boolean __VariableLimitSaturation_1;
41
       \exists boolean __VariableLimitSaturation_2;
42 42
       \exists real enforce_lo_lim;
43
       trans_VariableLimitSaturation(up_lim,
44
                                     Signal,
45
                                     lo_lim,
46
                                     out,
47
                                     __VariableLimitSaturation_1,
48
                                     __VariableLimitSaturation_2,
49
                                     enforce_lo_lim);
43
       trans_VariableLimitSaturation((up_lim),
44
                                     (Signal),
45
                                     (lo_lim),
46
                                     (out),
47
                                     (__VariableLimitSaturation_1?\true:\false),
48
                                     (__VariableLimitSaturation_2?\true:\false),
49
                                     (enforce_lo_lim));
50 50
*/
51 51
/*@ requires \valid(out);
52
  ensures Ctrans_VariableLimitSaturation(up_lim,
53
                                         Signal,
54
                                         lo_lim,
55
                                         *out);
52
  ensures Ctrans_VariableLimitSaturation((up_lim),
53
                                         (Signal),
54
                                         (lo_lim),
55
                                         (*out));
56 56
  assigns *out;
57 57
  */
58 58
extern void VariableLimitSaturation_step (double up_lim, double Signal,
......
61 61
                                          );
62 62

  
63 63
/*@ predicate trans_integrator_reset(real Fx,
64
                                     integer ResetLevel,
64
                                     boolean ResetLevel,
65 65
                                     real x0,
66 66
                                     real ir_out,
67 67
                                     struct integrator_reset_mem self1,
68 68
                                     struct integrator_reset_mem self2,
69
                                     integer __integrator_reset_1) =
69
                                     boolean __integrator_reset_1) =
70 70
       
71
       (__integrator_reset_1==(self1.ni_3._reg._first?(1):(0))) && (self2.ni_3._reg._first==0) &&
72
       (ir_out == (__integrator_reset_1?(x0):((ResetLevel?(x0):(((Fx * 1.) + self1._reg.__integrator_reset_2)))))) &&
73
       (self2._reg.__integrator_reset_2 == ir_out);
71
       ((__integrator_reset_1?\true:\false)==(self1.ni_3._reg._first?(1):(0))) && (self2.ni_3._reg._first==0) &&
72
       ((ir_out) == ((__integrator_reset_1?\true:\false)?((x0)):(((ResetLevel?\true:\false)?((x0)):((((Fx) * 1.) + self1._reg.__integrator_reset_2)))))) &&
73
       (self2._reg.__integrator_reset_2 == (ir_out));
74 74
*/
75 75
/*@ predicate Ctrans_integrator_reset(real Fx,
76
                                      integer ResetLevel,
76
                                      boolean ResetLevel,
77 77
                                      real x0,
78 78
                                      real ir_out,
79 79
                                      struct integrator_reset_mem self1,
80 80
                                      struct integrator_reset_mem self2) =
81
       \exists integer __integrator_reset_1;
82
       trans_integrator_reset(Fx,
83
                              ResetLevel,
84
                              x0,
85
                              ir_out,
81
       \exists boolean __integrator_reset_1;
82
       trans_integrator_reset((Fx),
83
                              (ResetLevel?\true:\false),
84
                              (x0),
85
                              (ir_out),
86 86
                              self1,
87 87
                              self2,
88
                              __integrator_reset_1);
88
                              (__integrator_reset_1?\true:\false));
89 89
*/
90 90
/*@ predicate init_integrator_reset(struct integrator_reset_mem self) =
91 91
       
......
108 108
/*@ requires \valid(ir_out);
109 109
  requires \valid(self);
110 110
  requires \separated(ir_out, self);
111
  ensures Ctrans_integrator_reset(Fx,
112
                                  ResetLevel,
113
                                  x0,
114
                                  *ir_out,
111
  ensures Ctrans_integrator_reset((Fx),
112
                                  (ResetLevel?\true:\false),
113
                                  (x0),
114
                                  (*ir_out),
115 115
                                  \at(*self, Pre),
116 116
                                  (*self));
117 117
  assigns *ir_out, *self;
......
122 122

  
123 123
/*@ predicate trans_Saturation(real Signal,
124 124
                               real s_out,
125
                               integer __Saturation_1,
126
                               integer __Saturation_2,
125
                               boolean __Saturation_1,
126
                               boolean __Saturation_2,
127 127
                               real enforce_lo_lim) =
128 128
       
129
       (__Saturation_1 == (0.0001 >= Signal)) &&
130
       (enforce_lo_lim == (__Saturation_1?(0.0001):(Signal))) &&
131
       (__Saturation_2 == (1000. <= enforce_lo_lim)) &&
132
       (s_out == (__Saturation_2?(1000.):(enforce_lo_lim)));
129
       ((__Saturation_1?\true:\false) == (0.0001 >= (Signal))) &&
130
       ((enforce_lo_lim) == ((__Saturation_1?\true:\false)?(0.0001):((Signal)))) &&
131
       ((__Saturation_2?\true:\false) == (1000. <= (enforce_lo_lim))) &&
132
       ((s_out) == ((__Saturation_2?\true:\false)?(1000.):((enforce_lo_lim))));
133 133
*/
134 134
/*@ predicate Ctrans_Saturation(real Signal,
135 135
                                real s_out) =
136
       \exists integer __Saturation_1;
137
       \exists integer __Saturation_2;
136
       \exists boolean __Saturation_1;
137
       \exists boolean __Saturation_2;
138 138
       \exists real enforce_lo_lim;
139
       trans_Saturation(Signal,
140
                        s_out,
141
                        __Saturation_1,
142
                        __Saturation_2,
143
                        enforce_lo_lim);
139
       trans_Saturation((Signal),
140
                        (s_out),
141
                        (__Saturation_1?\true:\false),
142
                        (__Saturation_2?\true:\false),
143
                        (enforce_lo_lim));
144 144
*/
145 145
/*@ requires \valid(s_out);
146
  ensures Ctrans_Saturation(Signal,
147
                            *s_out);
146
  ensures Ctrans_Saturation((Signal),
147
                            (*s_out));
148 148
  assigns *s_out;
149 149
  */
150 150
extern void Saturation_step (double Signal, 
......
153 153

  
154 154
/*@ predicate trans_VariableRateLimit(real ratelim_Out1_334,
155 155
                                      real input_Out1_344,
156
                                      integer ICtrig_Out1_354,
156
                                      boolean ICtrig_Out1_354,
157 157
                                      real IC_Out1_364,
158 158
                                      real output_In1_489,
159 159
                                      struct VariableRateLimit_mem self1,
......
163 163
                                      real Integrator1_Out1_391,
164 164
                                      real Sum2_Out1_401,
165 165
                                      real Variable_Limit_Saturation_Out1_410,
166
                                      integer __VariableRateLimit_1,
166
                                      boolean __VariableRateLimit_1,
167 167
                                      real __VariableRateLimit_2) =
168 168
       
169
       (__VariableRateLimit_1==(self1.ni_2._reg._first?(1):(0))) && (self2.ni_2._reg._first==0) &&
170
       (Integrator1_Out1_391 == (__VariableRateLimit_1?(IC_Out1_364):(self1._reg.__VariableRateLimit_3))) &&
171
       (output_In1_489 == Integrator1_Out1_391) &&
172
       (Gain1_Out1_382 == (- ratelim_Out1_334)) &&
173
       (Sum2_Out1_401 == (input_Out1_344 + (- Integrator1_Out1_391))) &&
174
       (Gain_Out1_373 == (20. * Sum2_Out1_401)) &&
175
       Ctrans_VariableLimitSaturation((double) ratelim_Out1_334,
176
                                      (double) Gain_Out1_373,
177
                                      (double) Gain1_Out1_382,
178
                                      Variable_Limit_Saturation_Out1_410) &&
179
       Ctrans_integrator_reset((double) Variable_Limit_Saturation_Out1_410,
180
                               (_Bool) ICtrig_Out1_354,
181
                               (double) IC_Out1_364,
182
                               __VariableRateLimit_2,
169
       ((__VariableRateLimit_1?\true:\false)==(self1.ni_2._reg._first?(1):(0))) && (self2.ni_2._reg._first==0) &&
170
       ((Integrator1_Out1_391) == ((__VariableRateLimit_1?\true:\false)?((IC_Out1_364)):(self1._reg.__VariableRateLimit_3))) &&
171
       ((output_In1_489) == (Integrator1_Out1_391)) &&
172
       ((Gain1_Out1_382) == (- (ratelim_Out1_334))) &&
173
       ((Sum2_Out1_401) == ((input_Out1_344) + (- (Integrator1_Out1_391)))) &&
174
       ((Gain_Out1_373) == (20. * (Sum2_Out1_401))) &&
175
       Ctrans_VariableLimitSaturation((ratelim_Out1_334),
176
                                      (Gain_Out1_373),
177
                                      (Gain1_Out1_382),
178
                                      (Variable_Limit_Saturation_Out1_410)) &&
179
       Ctrans_integrator_reset((Variable_Limit_Saturation_Out1_410),
180
                               (ICtrig_Out1_354?\true:\false),
181
                               (IC_Out1_364),
182
                               (__VariableRateLimit_2),
183 183
                               self1.ni_1,
184 184
                               self2.ni_1) &&
185
       (self2._reg.__VariableRateLimit_3 == __VariableRateLimit_2);
185
       (self2._reg.__VariableRateLimit_3 == (__VariableRateLimit_2));
186 186
*/
187 187
/*@ predicate Ctrans_VariableRateLimit(real ratelim_Out1_334,
188 188
                                       real input_Out1_344,
189
                                       integer ICtrig_Out1_354,
189
                                       boolean ICtrig_Out1_354,
190 190
                                       real IC_Out1_364,
191 191
                                       real output_In1_489,
192 192
                                       struct VariableRateLimit_mem self1,
......
196 196
       \exists real Integrator1_Out1_391;
197 197
       \exists real Sum2_Out1_401;
198 198
       \exists real Variable_Limit_Saturation_Out1_410;
199
       \exists integer __VariableRateLimit_1;
199
       \exists boolean __VariableRateLimit_1;
200 200
       \exists real __VariableRateLimit_2;
201
       trans_VariableRateLimit(ratelim_Out1_334,
202
                               input_Out1_344,
203
                               ICtrig_Out1_354,
204
                               IC_Out1_364,
205
                               output_In1_489,
201
       trans_VariableRateLimit((ratelim_Out1_334),
202
                               (input_Out1_344),
203
                               (ICtrig_Out1_354?\true:\false),
204
                               (IC_Out1_364),
205
                               (output_In1_489),
206 206
                               self1,
207 207
                               self2,
208
                               Gain1_Out1_382,
209
                               Gain_Out1_373,
210
                               Integrator1_Out1_391,
211
                               Sum2_Out1_401,
212
                               Variable_Limit_Saturation_Out1_410,
213
                               __VariableRateLimit_1,
214
                               __VariableRateLimit_2);
208
                               (Gain1_Out1_382),
209
                               (Gain_Out1_373),
210
                               (Integrator1_Out1_391),
211
                               (Sum2_Out1_401),
212
                               (Variable_Limit_Saturation_Out1_410),
213
                               (__VariableRateLimit_1?\true:\false),
214
                               (__VariableRateLimit_2));
215 215
*/
216 216
/*@ predicate init_VariableRateLimit(struct VariableRateLimit_mem self) =
217 217
       
......
236 236
/*@ requires \valid(output_In1_489);
237 237
  requires \valid(self);
238 238
  requires \separated(output_In1_489, self);
239
  ensures Ctrans_VariableRateLimit(ratelim_Out1_334,
240
                                   input_Out1_344,
241
                                   ICtrig_Out1_354,
242
                                   IC_Out1_364,
243
                                   *output_In1_489,
239
  ensures Ctrans_VariableRateLimit((ratelim_Out1_334),
240
                                   (input_Out1_344),
241
                                   (ICtrig_Out1_354?\true:\false),
242
                                   (IC_Out1_364),
243
                                   (*output_In1_489),
244 244
                                   \at(*self, Pre),
245 245
                                   (*self));
246 246
  assigns *output_In1_489, *self;
......
269 269
                                    struct AltitudeControl_mem self2,
270 270
                                    real Abs_Out1_144,
271 271
                                    real Kh_Out1_193,
272
                                    integer Logical_Operator_In1_197,
273
                                    integer Logical_Operator_Out1_198,
272
                                    boolean Logical_Operator_In1_197,
273
                                    boolean Logical_Operator_Out1_198,
274 274
                                    real Saturation1_Out1_213,
275 275
                                    real Sum3_Out1_296,
276 276
                                    real Sum_Out1_286,
277
                                    integer Switch1_In2_312,
277
                                    boolean Switch1_In2_312,
278 278
                                    real Switch1_Out1_314,
279
                                    integer Switch_In2_303,
279
                                    boolean Switch_In2_303,
280 280
                                    real Switch_Out1_305,
281 281
                                    real Variable_Limit_Saturation_0_Out1_509,
282 282
                                    real Variable__Rate_Limit_Out1_324,
283
                                    integer __AltitudeControl_1,
284
                                    integer __AltitudeControl_2,
283
                                    boolean __AltitudeControl_1,
284
                                    boolean __AltitudeControl_2,
285 285
                                    real k_Out1_585,
286 286
                                    real kts2fps_Out1_594,
287 287
                                    real r2d_Out1_603) =
288 288
       
289
       (__AltitudeControl_1 == (hdot_Out1_59 < 0.)) &&
290
       (Abs_Out1_144 == (__AltitudeControl_1?((- hdot_Out1_59)):(hdot_Out1_59))) &&
291
       (Sum3_Out1_296 == (Abs_Out1_144 + 10.)) &&
292
       (k_Out1_585 == (- Sum3_Out1_296)) &&
293
       (__AltitudeControl_2 == (AntEng_Out1_19 == 0.)) &&
294
       ((!Logical_Operator_In1_197) == (!(__AltitudeControl_2?(0):(1)))) &&
295
       ((!Logical_Operator_Out1_198) == (!(!Logical_Operator_In1_197))) &&
296
       ((!Switch_In2_303) == (!(__AltitudeControl_2?(0):(1)))) &&
297
       (Sum_Out1_286 == (AltCmd_Out1_29 + (- Alt_Out1_39))) &&
298
       (Kh_Out1_193 == (0.08 * Sum_Out1_286)) &&
299
       (Switch_Out1_305 == (Switch_In2_303?(Kh_Out1_193):(0.))) &&
300
       Ctrans_VariableLimitSaturation((double) Sum3_Out1_296,
301
                                      (double) Switch_Out1_305,
302
                                      (double) k_Out1_585,
303
                                      Variable_Limit_Saturation_0_Out1_509) &&
304
       Ctrans_VariableRateLimit((double) hdotChgRate_Out1_69,
305
                                (double) Variable_Limit_Saturation_0_Out1_509,
306
                                (_Bool) Logical_Operator_Out1_198,
307
                                (double) hdot_Out1_59,
308
                                Variable__Rate_Limit_Out1_324,
289
       ((__AltitudeControl_1?\true:\false) == ((hdot_Out1_59) < 0.)) &&
290
       ((Abs_Out1_144) == ((__AltitudeControl_1?\true:\false)?((- (hdot_Out1_59))):((hdot_Out1_59)))) &&
291
       ((Sum3_Out1_296) == ((Abs_Out1_144) + 10.)) &&
292
       ((k_Out1_585) == (- (Sum3_Out1_296))) &&
293
       ((__AltitudeControl_2?\true:\false) == ((AntEng_Out1_19) == 0.)) &&
294
       ((!(Logical_Operator_In1_197?\true:\false)) == (!((__AltitudeControl_2?\true:\false)?(0):(1)))) &&
295
       ((!(Logical_Operator_Out1_198?\true:\false)) == (!(!(Logical_Operator_In1_197?\true:\false)))) &&
296
       ((!(Switch_In2_303?\true:\false)) == (!((__AltitudeControl_2?\true:\false)?(0):(1)))) &&
297
       ((Sum_Out1_286) == ((AltCmd_Out1_29) + (- (Alt_Out1_39)))) &&
298
       ((Kh_Out1_193) == (0.08 * (Sum_Out1_286))) &&
299
       ((Switch_Out1_305) == ((Switch_In2_303?\true:\false)?((Kh_Out1_193)):(0.))) &&
300
       Ctrans_VariableLimitSaturation((Sum3_Out1_296),
301
                                      (Switch_Out1_305),
302
                                      (k_Out1_585),
303
                                      (Variable_Limit_Saturation_0_Out1_509)) &&
304
       Ctrans_VariableRateLimit((hdotChgRate_Out1_69),
305
                                (Variable_Limit_Saturation_0_Out1_509),
306
                                (Logical_Operator_Out1_198?\true:\false),
307
                                (hdot_Out1_59),
308
                                (Variable__Rate_Limit_Out1_324),
309 309
                                self1.ni_0,
310 310
                                self2.ni_0) &&
311
       (r2d_Out1_603 == (57.2958 * Variable__Rate_Limit_Out1_324)) &&
312
       (kts2fps_Out1_594 == (1.6878 * GsKts_Out1_49)) &&
313
       ((!Switch1_In2_312) == (!(__AltitudeControl_2?(0):(1)))) &&
314
       (Switch1_Out1_314 == (Switch1_In2_312?(r2d_Out1_603):(0.))) &&
315
       (altgammacmd_In1_661 == Switch1_Out1_314) &&
316
       Ctrans_Saturation((double) kts2fps_Out1_594,
317
                         Saturation1_Out1_213);
311
       ((r2d_Out1_603) == (57.2958 * (Variable__Rate_Limit_Out1_324))) &&
312
       ((kts2fps_Out1_594) == (1.6878 * (GsKts_Out1_49))) &&
313
       ((!(Switch1_In2_312?\true:\false)) == (!((__AltitudeControl_2?\true:\false)?(0):(1)))) &&
314
       ((Switch1_Out1_314) == ((Switch1_In2_312?\true:\false)?((r2d_Out1_603)):(0.))) &&
315
       ((altgammacmd_In1_661) == (Switch1_Out1_314)) &&
316
       Ctrans_Saturation((kts2fps_Out1_594),
317
                         (Saturation1_Out1_213));
318 318
*/
319 319
/*@ predicate Ctrans_AltitudeControl(real AntEng_Out1_19,
320 320
                                     real AltCmd_Out1_29,
......
327 327
                                     struct AltitudeControl_mem self2) =
328 328
       \exists real Abs_Out1_144;
329 329
       \exists real Kh_Out1_193;
330
       \exists integer Logical_Operator_In1_197;
331
       \exists integer Logical_Operator_Out1_198;
330
       \exists boolean Logical_Operator_In1_197;
331
       \exists boolean Logical_Operator_Out1_198;
332 332
       \exists real Saturation1_Out1_213;
333 333
       \exists real Sum3_Out1_296;
334 334
       \exists real Sum_Out1_286;
335
       \exists integer Switch1_In2_312;
335
       \exists boolean Switch1_In2_312;
336 336
       \exists real Switch1_Out1_314;
337
       \exists integer Switch_In2_303;
337
       \exists boolean Switch_In2_303;
338 338
       \exists real Switch_Out1_305;
339 339
       \exists real Variable_Limit_Saturation_0_Out1_509;
340 340
       \exists real Variable__Rate_Limit_Out1_324;
341
       \exists integer __AltitudeControl_1;
342
       \exists integer __AltitudeControl_2;
341
       \exists boolean __AltitudeControl_1;
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff