diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-06-26 22:02:02 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-06-26 22:02:02 +0200 |
| commit | e24e4a9329885c80fbbb42a1c541880eff607e32 (patch) | |
| tree | 01f2995f0dbce61599c141d10d493407bad95295 /backend/Asmexpandaux.ml | |
| parent | 777566e81b9762d6bdc773a1f63d56a7ac97433c (diff) | |
| download | compcert-kvx-e24e4a9329885c80fbbb42a1c541880eff607e32.tar.gz compcert-kvx-e24e4a9329885c80fbbb42a1c541880eff607e32.zip | |
Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert"
This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing
changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1.
Diffstat (limited to 'backend/Asmexpandaux.ml')
| -rw-r--r-- | backend/Asmexpandaux.ml | 57 |
1 files changed, 0 insertions, 57 deletions
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml deleted file mode 100644 index 6ce6c005..00000000 --- a/backend/Asmexpandaux.ml +++ /dev/null @@ -1,57 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Util functions used for the expansion of built-ins and some - pseudo-instructions *) - -open Asm -open AST -open Camlcoq - -(* Buffering the expanded code *) - -let current_code = ref ([]: instruction list) - -let emit i = current_code := i :: !current_code - -(* Generation of fresh labels *) - -let dummy_function = { fn_code = []; fn_sig = signature_main } -let current_function = ref dummy_function -let next_label = ref (None: label option) - -let new_label () = - let lbl = - match !next_label with - | Some l -> l - | None -> - (* on-demand computation of the next available label *) - List.fold_left - (fun next instr -> - match instr with - | Plabel l -> if P.lt l next then next else P.succ l - | _ -> next) - P.one (!current_function).fn_code - in - next_label := Some (P.succ lbl); - lbl - - -let set_current_function f = - current_function := f; next_label := None; current_code := [] - -let get_current_function () = - let c = List.rev !current_code in - let fn = !current_function in - set_current_function dummy_function; - {fn with fn_code = c} |