diff options
Diffstat (limited to 'arm/CBuiltins.ml')
| -rw-r--r-- | arm/CBuiltins.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml index b9b54e4..4446ab2 100644 --- a/arm/CBuiltins.ml +++ b/arm/CBuiltins.ml @@ -43,6 +43,11 @@ let builtins = { (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false); "__builtin_write32_reversed", (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false); + (* Synchronization *) + "__builtin_dsb", + (TVoid [], [], false); + "__builtin_isb", + (TVoid [], [], false) ] } |