(* *********************************************************************) (* *) (* 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 INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) (* Expanding built-ins and some pseudo-instructions by rewriting of the ARM assembly code. Currently not done, this expansion is performed on the fly in PrintAsm. *) let expand_program p = p