diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-11 12:14:33 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-11 12:14:33 +0200 |
| commit | 71bfa128316019b0199db87acdf31deb9f9e7405 (patch) | |
| tree | 141abac0b985cbf2904e68df40309fb9fda18cfc /mppa_k1c/CBuiltins.ml | |
| parent | e93ef3ef5f0925ce6b99208157a49a99032c1f87 (diff) | |
| download | compcert-kvx-71bfa128316019b0199db87acdf31deb9f9e7405.tar.gz compcert-kvx-71bfa128316019b0199db87acdf31deb9f9e7405.zip | |
some more builtins
Diffstat (limited to 'mppa_k1c/CBuiltins.ml')
| -rw-r--r-- | mppa_k1c/CBuiltins.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml index 0de6d0c7..e4652d77 100644 --- a/mppa_k1c/CBuiltins.ml +++ b/mppa_k1c/CBuiltins.ml @@ -24,8 +24,8 @@ let builtins = { (* The builtin list is inspired from the GCC file builtin_k1.h *) Builtins.functions = [ (* Some builtins are commented out because their opcode is not present (yet?) *) (* BCU Instructions *) - "__builtin_k1_await", (TVoid [], [], false); - "__builtin_k1_barrier", (TVoid [], [], false); + "__builtin_k1_await", (TVoid [], [], false); (* DONE *) + "__builtin_k1_barrier", (TVoid [], [], false); (* DONE *) "__builtin_k1_doze", (TVoid [], [], false); "__builtin_k1_wfxl", (TVoid [], [TInt(IUChar, []); TInt(ILongLong, [])], false); (* DONE *) "__builtin_k1_wfxm", (TVoid [], [TInt(IUChar, []); TInt(ILongLong, [])], false); (* DONE *) @@ -33,8 +33,8 @@ let builtins = { "__builtin_k1_invalitlb", (TVoid [], [], false); "__builtin_k1_probetlb", (TVoid [], [], false); "__builtin_k1_readtlb", (TVoid [], [], false); - "__builtin_k1_sleep", (TVoid [], [], false); - "__builtin_k1_stop", (TVoid [], [], false); + "__builtin_k1_sleep", (TVoid [], [], false); (* DONE *) + "__builtin_k1_stop", (TVoid [], [], false); (* DONE *) "__builtin_k1_syncgroup", (TVoid [], [TInt(IUInt, [])], false); "__builtin_k1_tlbwrite", (TVoid [], [], false); @@ -49,7 +49,7 @@ let builtins = { "__builtin_k1_dinvall", (TVoid [], [TPtr(TVoid [], [])], false); "__builtin_k1_dtouchl", (TVoid [], [TPtr(TVoid [], [])], false); "__builtin_k1_dzerol", (TVoid [], [TPtr(TVoid [], [])], false); - "__builtin_k1_fence", (TVoid [], [], false); + "__builtin_k1_fence", (TVoid [], [], false); (* DONE *) "__builtin_k1_iinval", (TVoid [], [], false); "__builtin_k1_iinvals", (TVoid [], [TPtr(TVoid [], [])], false); "__builtin_k1_itouchl", (TVoid [], [TPtr(TVoid [], [])], false); |