From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:08:29 +0000 Subject: Fusion de la branche "traces": - Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Lineartyping.v | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'backend/Lineartyping.v') diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 0b13b40a..bf41908b 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -38,6 +38,7 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lstore chunk addr args src => src :: args | Lcall sig (inl fn) => fn :: nil | Lcall sig (inr _) => nil + | Lalloc => nil | Llabel lbl => nil | Lgoto lbl => nil | Lcond cond args lbl => args @@ -231,6 +232,8 @@ Inductive wt_instr : instruction -> Prop := size_arguments sig <= bound_outgoing b -> match ros with inl r => mreg_type r = Tint | _ => True end -> wt_instr (Lcall sig ros) + | wt_Lalloc: + wt_instr Lalloc | wt_Llabel: forall lbl, wt_instr (Llabel lbl) @@ -249,6 +252,14 @@ End WT_INSTR. Definition wt_function (f: function) : Prop := forall instr, In instr f.(fn_code) -> wt_instr f instr. +Inductive wt_fundef: fundef -> Prop := + | wt_fundef_external: forall ef, + Conventions.sig_external_ok ef.(ef_sig) -> + wt_fundef (External ef) + | wt_function_internal: forall f, + wt_function f -> + wt_fundef (Internal f). + Definition wt_program (p: program) : Prop := - forall i f, In (i, f) (prog_funct p) -> wt_function f. + forall i f, In (i, f) (prog_funct p) -> wt_fundef f. -- cgit