diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-11 21:36:57 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-11 21:36:57 +0100 |
| commit | 16715e5efd6ce899eb3d544fd71751f367eaa370 (patch) | |
| tree | fb5cc283dec59bf362a4515e0212165832e5b0a9 /kvx/CBuiltins.ml | |
| parent | bc33b3536cc9985a6dddacadfaa9c2f5a111f4ac (diff) | |
| download | compcert-kvx-16715e5efd6ce899eb3d544fd71751f367eaa370.tar.gz compcert-kvx-16715e5efd6ce899eb3d544fd71751f367eaa370.zip | |
modulos
Diffstat (limited to 'kvx/CBuiltins.ml')
| -rw-r--r-- | kvx/CBuiltins.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kvx/CBuiltins.ml b/kvx/CBuiltins.ml index 49534867..5ca5ddba 100644 --- a/kvx/CBuiltins.ml +++ b/kvx/CBuiltins.ml @@ -141,6 +141,10 @@ let builtins = { (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false); "__builtin_fp_udiv64", (TInt(IULong, []), [TInt(IULong, []); TInt(IULong, [])], false); + "__builtin_fp_umod32", + (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false); + "__builtin_fp_umod64", + (TInt(IULong, []), [TInt(IULong, []); TInt(IULong, [])], false); ] } |