diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-28 15:22:31 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-28 15:22:31 +0000 |
commit | 26eb2a1350dcf0355c58c45e300d593204affb83 (patch) | |
tree | f2d3977d4e71d712d8f8094c4cd622fde03f9bae | |
parent | 484bf49d18cb98817a95183827fea469b4367a40 (diff) | |
download | compcert-26eb2a1350dcf0355c58c45e300d593204affb83.tar.gz compcert-26eb2a1350dcf0355c58c45e300d593204affb83.zip |
Typo in arm/PrintAsm.ml
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1690 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r-- | arm/PrintAsm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 44a7571d..4406f5b8 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -323,7 +323,7 @@ let print_builtin_memcpy oc sz al args = fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n" comment sz al; let n = - if sz <= 64 + if sz <= 32 then print_builtin_memcpy_small oc sz al src dst else print_builtin_memcpy_big oc sz al src dst in fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment; n @@ -646,7 +646,7 @@ let print_fundef oc (Coq_pair(name, defn)) = match defn with | Internal code -> print_function oc name code - | External ef + | External ef -> if need_stub ef then print_external_function oc name (ef_sig ef) (* Data *) |