aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/CBuiltins.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-08-21 17:53:44 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-08-21 17:53:44 +0200
commit4f187fdafdac0cf4a8b83964c89d79741dbd813e (patch)
treed99aa80714b2b07817133ea8e4fc00a16f4b0adf /powerpc/CBuiltins.ml
parent84c3580d0514c24a7c29eeec635e16183c3c5c65 (diff)
downloadcompcert-4f187fdafdac0cf4a8b83964c89d79741dbd813e.tar.gz
compcert-4f187fdafdac0cf4a8b83964c89d79741dbd813e.zip
Adapt the PowerPC port to the new builtin representation.
__builtin_get_spr() and __builtin_set_spr() work, but horrible error message if the SPR argument is not a constant. powerpc/AsmToJSON.ml needs updating.
Diffstat (limited to 'powerpc/CBuiltins.ml')
-rw-r--r--powerpc/CBuiltins.ml7
1 files changed, 6 insertions, 1 deletions
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 06a7e395..75dbd23d 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -93,7 +93,12 @@ let builtins = {
"__builtin_dcbi",
(TVoid [],[TPtr(TVoid [], [])],false);
"__builtin_icbi",
- (TVoid [],[TPtr(TVoid [], [])],false)
+ (TVoid [],[TPtr(TVoid [], [])],false);
+ (* Access to special registers *)
+ "__builtin_get_spr",
+ (TInt(IUInt, []), [TInt(IInt, [])], false);
+ "__builtin_set_spr",
+ (TVoid [], [TInt(IInt, []); TInt(IUInt, [])], false)
]
}