diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-05-21 16:26:30 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-05-21 16:26:30 +0000 |
commit | 0053b1aa1d26da5d1f995a603b127daf799c2da9 (patch) | |
tree | fec49ad37e5edffa5be742bafcadff3c8b8ede7f /backend/PrintLTLin.ml | |
parent | 219a2d178dcd5cc625f6b6261759f392cfca367b (diff) | |
download | compcert-0053b1aa1d26da5d1f995a603b127daf799c2da9.tar.gz compcert-0053b1aa1d26da5d1f995a603b127daf799c2da9.zip |
Merge of the newmem branch:
- Revised memory model with Max and Cur permissions, but without bounds
- Constant propagation of 'const' globals
- Function inlining at RTL level
- (Unprovable) elimination of unreferenced static definitions
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/PrintLTLin.ml')
-rw-r--r-- | backend/PrintLTLin.ml | 27 |
1 files changed, 12 insertions, 15 deletions
diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml index adff4834..bb360eb3 100644 --- a/backend/PrintLTLin.ml +++ b/backend/PrintLTLin.ml @@ -90,29 +90,26 @@ let print_instruction pp i = | Lreturn (Some arg) -> fprintf pp "return %a@ " reg arg -let print_function pp f = - fprintf pp "@[<v 2>f(%a) {@ " regs f.fn_params; +let print_function pp id f = + fprintf pp "@[<v 2>%s(%a) {@ " (extern_atom id) regs f.fn_params; List.iter (print_instruction pp) f.fn_code; fprintf pp "@;<0 -2>}@]@." -let print_fundef pp fd = +let print_fundef pp (id, fd) = match fd with - | Internal f -> print_function pp f + | Internal f -> print_function pp id f | External _ -> () +let print_program pp prog = + List.iter (print_fundef pp) prog.prog_funct + let destination : string option ref = ref None -let currpp : formatter option ref = ref None -let print_if fd = +let print_if prog = match !destination with | None -> () | Some f -> - let pp = - match !currpp with - | Some pp -> pp - | None -> - let oc = open_out f in - let pp = formatter_of_out_channel oc in - currpp := Some pp; - pp - in print_fundef pp fd + let oc = open_out f in + let pp = formatter_of_out_channel oc in + print_program pp prog; + close_out oc |