diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2020-01-02 15:02:20 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-01-03 09:12:23 +0100 |
| commit | 2696f9b4a626229879248d7c97de252619a4e3b2 (patch) | |
| tree | abbe564a7d0a7edf254f7539f6e979e97fc22263 /x86 | |
| parent | 7077c2ea9e86f001e805d7a2a5e7fcdfd0a8ece8 (diff) | |
| download | compcert-kvx-2696f9b4a626229879248d7c97de252619a4e3b2.tar.gz compcert-kvx-2696f9b4a626229879248d7c97de252619a4e3b2.zip | |
Remove __builtin_nop from list of x86 builtins.
Diffstat (limited to 'x86')
| -rw-r--r-- | x86/CBuiltins.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml index f4f40a31..e7f714c7 100644 --- a/x86/CBuiltins.ml +++ b/x86/CBuiltins.ml @@ -73,9 +73,6 @@ 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); ] } |