diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-27 07:35:49 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-27 07:35:49 +0000 |
| commit | f4e106d4fc1cce484678b5cdd86ab57d7a43076a (patch) | |
| tree | 3de9bddc63b80fb1b695bbdb8fa5bd6aa893a13a /extraction | |
| parent | 04ff02a9f4bc4f766a450e5463729102ee26882e (diff) | |
ARM port: add support for Thumb2. To be tested.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2549 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 0f23264..f0033af 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -93,6 +93,8 @@ Extract Constant Compopts.generate_float_constants => "fun _ -> !Clflags.option_ffloatconstprop >= 2". Extract Constant Compopts.eliminate_tailcalls => "fun _ -> !Clflags.option_ftailcalls". +Extract Constant Compopts.thumb => + "fun _ -> !Clflags.option_fthumb". (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". |