source: src/Clight/test/sum.test.ma @ 1631

include "Clight/test/sum.c.ma".

example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
normalize  (* you can examine the result here *)
@refl
qed.

include "Clight/SimplifyCasts.ma".

example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]).
normalize  (* you can examine the result here *)
@refl
qed.

include "Clight/toCminor.ma".
include "Cminor/semantics.ma".

example e1: finishes_with (repr I32 74) ?
  (bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
   (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
normalize
@refl
qed.

include "Cminor/toRTLabs.ma".
include "RTLabs/semantics.ma".

example e2: finishes_with (repr I32 74) ? (
bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
(λp1. bind ? (snapshot state) (cminor_to_rtlabs p1)
 (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ]))).
normalize
@refl
qed.
(*
include "RTLabs/RTLabsToRTL.ma".
include alias "basics/lists/list.ma".

definition take_out: ∀A. res A → A ≝
 λA,a. match a with [ OK x ⇒ x | Error _ ⇒ ?].
cases daemon
qed.

example CSC: True.
letin xxx ≝
 (let p ≝ take_out … (clight_to_cminor myprog) in
  let p ≝ take_out … (cminor_to_rtlabs p) in
(*   (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)) *)
  let p ≝ rtlabs_to_rtl p in
   (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ joint_if_code … f]) (prog_funct … p))
 )
[2: cases daemon]
normalize in xxx;


[2:
  OK (list (codeT (prog_var_names … p) (rtl_params (prog_var_names … p)))) (list_map … (λx. match (\snd x) return λ_.codeT (prog_var_names … p) (rtl_params ?) with [External _ ⇒ ? | Internal f ⇒ ?(*joint_if_code ? (rtl_params ?) f*)]) (prog_funct … p)))
(*  OK ? (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)))
*)
[2: check (joint_if_code (prog_var_names … p) ? f) |3: cases daemon  ]
normalize in xxx
*)