diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-11 15:32:05 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-11 15:32:05 +0200 |
| commit | fa27e482f043116bb39ff4d410f12f0b09a18f3b (patch) | |
| tree | 40b009f7f1590f39678551f71ebde12b2623c00f /mppa_k1c | |
| parent | 0e5f7395d185cde931c11fb3a12e6c2af03a7ebf (diff) | |
| download | compcert-kvx-fa27e482f043116bb39ff4d410f12f0b09a18f3b.tar.gz compcert-kvx-fa27e482f043116bb39ff4d410f12f0b09a18f3b.zip | |
adjust list of builtins according to documentation
Diffstat (limited to 'mppa_k1c')
| -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 9fe5c958..914d1aa8 100644 --- a/mppa_k1c/CBuiltins.ml +++ b/mppa_k1c/CBuiltins.ml @@ -29,14 +29,14 @@ let builtins = { "__builtin_k1_doze", (TVoid [], [], false); (* opcode not supported in assembly, not in documentation *) "__builtin_k1_wfxl", (TVoid [], [TInt(IUChar, []); TInt(ILongLong, [])], false); (* DONE *) "__builtin_k1_wfxm", (TVoid [], [TInt(IUChar, []); TInt(ILongLong, [])], false); (* DONE *) - "__builtin_k1_invaldtlb", (TVoid [], [], false); - "__builtin_k1_invalitlb", (TVoid [], [], false); - "__builtin_k1_probetlb", (TVoid [], [], false); - "__builtin_k1_readtlb", (TVoid [], [], false); "__builtin_k1_sleep", (TVoid [], [], false); (* DONE *) "__builtin_k1_stop", (TVoid [], [], false); (* DONE *) - "__builtin_k1_syncgroup", (TVoid [], [TInt(IUInt, [])], false); + "__builtin_k1_syncgroup", (TVoid [], [TInt(IULongLong, [])], false); + "__builtin_k1_tlbread", (TVoid [], [], false); "__builtin_k1_tlbwrite", (TVoid [], [], false); + "__builtin_k1_tlbprobe", (TVoid [], [], false); + "__builtin_k1_tlbdinval", (TVoid [], [], false); + "__builtin_k1_tlbiinval", (TVoid [], [], false); "__builtin_k1_get", (TInt(IULongLong, []), [TInt(IInt, [])], false); (* DONE *) "__builtin_k1_set", (TVoid [], [TInt(IInt, []); TInt(IULongLong, [])], false); (* DONE *) |