diff options
| -rw-r--r-- | driver/Compiler.vexpand | 18 | ||||
| -rw-r--r-- | tools/compiler_expand.ml | 10 |
2 files changed, 19 insertions, 9 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 1e671464..0f59aab7 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -208,15 +208,15 @@ Theorem transf_c_program_match: match_prog p tp. Proof. intros p tp T. - unfold transf_c_program, time in T. simpl in T. - destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. - unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. - destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. - destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. - unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. - destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. + unfold transf_c_program, time in T. cbn in T. + destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; cbn in T; try discriminate. + unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. cbn in T. + destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; cbn in T; try discriminate. + destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; cbn in T; try discriminate. + destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; cbn in T; try discriminate. + unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. cbn in T. + destruct (Selection.sel_program p4) as [p5|e] eqn:P5; cbn in T; try discriminate. + destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; cbn in T; try discriminate. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. cbn in T. EXPAND_RTL_PROOF diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 4fc746f0..960d1ce1 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -1,3 +1,13 @@ +(* +The Compcert verified compiler + +Compiler.vexpand -> Compiler.v + +Expand the list of RTL compiler passes into Compiler.v + +David Monniaux, CNRS, VERIMAG + *) + type is_partial = TOTAL | PARTIAL;; type print_result = Noprint | Print of string;; type when_triggered = Always | Option of string;; |