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 *)