From e24e4a9329885c80fbbb42a1c541880eff607e32 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 26 Jun 2015 22:02:02 +0200 Subject: Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert" This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1. --- backend/Asmexpandaux.ml | 57 ------------------------------------------------- 1 file changed, 57 deletions(-) delete mode 100644 backend/Asmexpandaux.ml (limited to 'backend/Asmexpandaux.ml') 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} -- cgit