diff options
| author | Michael Schmidt <github@mschmidt.me> | 2015-12-11 10:15:33 +0100 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2015-12-11 10:15:33 +0100 |
| commit | 66ae780e8a94f676480e9eec40354a3a8cbc3041 (patch) | |
| tree | c45a1c3471eb2cf93f1fb7fc7cd3a4c910890847 /powerpc/CBuiltins.ml | |
| parent | a7f005b94a1dac82ac106950f643507a268ff1c9 (diff) | |
| download | compcert-kvx-66ae780e8a94f676480e9eec40354a3a8cbc3041.tar.gz compcert-kvx-66ae780e8a94f676480e9eec40354a3a8cbc3041.zip | |
bug 17752, add builtin_nop for PowerPC
Diffstat (limited to 'powerpc/CBuiltins.ml')
| -rwxr-xr-x | powerpc/CBuiltins.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 6efeff17..a611aabe 100755 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -122,6 +122,9 @@ let builtins = { (* uisel *) "__builtin_uisel", (TInt (IUInt, []),[TInt(IBool, []);TInt(IUInt, []);TInt(IUInt, [])],false); + (* no operation *) + "__builtin_nop", + (TVoid [], [], false); (* atomic operations *) "__builtin_atomic_exchange", (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false); |