aboutsummaryrefslogtreecommitdiffstats
path: root/x86/CBuiltins.ml
diff options
context:
space:
mode:
Diffstat (limited to 'x86/CBuiltins.ml')
-rw-r--r--x86/CBuiltins.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml
index e7f714c7..f4f40a31 100644
--- a/x86/CBuiltins.ml
+++ b/x86/CBuiltins.ml
@@ -73,6 +73,9 @@ let builtins = {
(TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false);
"__builtin_write32_reversed",
(TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
+ (* no operation *)
+ "__builtin_nop",
+ (TVoid [], [], false);
]
}