diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
| commit | 355b4abcee015c3fae9ac5653c25259e104a886c (patch) | |
| tree | cfdb5b17f36b815bb358699cf420f64eba9dfe25 /caml/PrintPPC.ml | |
| parent | 22ff08b38616ceef336f5f974d4edc4d37d955e8 (diff) | |
Fusion des modifications faites sur les branches "tailcalls" et "smallstep".
En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml/PrintPPC.ml')
| -rw-r--r-- | caml/PrintPPC.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml index 3ee79d1..bf7b2cc 100644 --- a/caml/PrintPPC.ml +++ b/caml/PrintPPC.ml @@ -137,6 +137,8 @@ let print_instruction oc labels = function fprintf oc " bf %a, %a\n" print_crbit bit print_label lbl | Pbl s -> fprintf oc " bl %a\n" print_symb s + | Pbs s -> + fprintf oc " b %a\n" print_symb s | Pblr -> fprintf oc " blr\n" | Pbt(bit, lbl) -> @@ -318,10 +320,6 @@ let print_instruction oc labels = function fprintf oc " xoris %a, %a, %a\n" ireg r1 ireg r2 print_constant c | Plabel lbl -> if Labelset.mem lbl labels then fprintf oc "%a:\n" print_label lbl - | Piundef r -> - fprintf oc " # undef %a\n" ireg r - | Pfundef r -> - fprintf oc " # undef %a\n" freg r let rec labels_of_code = function | Coq_nil -> Labelset.empty |