From 913c1bcc4b2204afd447edd723e06b905fd1f47f Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 8 May 2010 14:32:58 +0000 Subject: Cleaned up handling of linker sections. Minor updates on ARM code generator. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1339 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Sections.mli | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 common/Sections.mli (limited to 'common/Sections.mli') diff --git a/common/Sections.mli b/common/Sections.mli new file mode 100644 index 00000000..090d4bbb --- /dev/null +++ b/common/Sections.mli @@ -0,0 +1,43 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + + +(* Handling of linker sections *) + +type section_name = + | Section_text + | Section_data of bool (* true = init data, false = uninit data *) + | Section_small_data of bool + | Section_const + | Section_small_const + | Section_string + | Section_literal + | Section_jumptable + | Section_user of string * bool (*writable*) * bool (*executable*) + +val initialize: unit -> unit + +val define_section: + string -> ?iname:string -> ?uname:string + -> ?writable:bool -> ?executable:bool -> ?near:bool -> unit -> unit +val use_section_for: AST.ident -> string -> bool + +val define_function: AST.ident -> unit +val define_variable: AST.ident -> int -> bool -> unit +val define_stringlit: AST.ident -> unit + +val section_for_variable: AST.ident -> bool -> section_name +val sections_for_function: AST.ident -> section_name * section_name * section_name +val atom_is_small_data: AST.ident -> Integers.Int.int -> bool -- cgit