diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 20:19:24 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 20:19:24 +0200 |
| commit | 2dca62f38463b0ebce24fff50666c846df50488e (patch) | |
| tree | 356c1eeb4d084002efd5ea28fdd83ecdf7ed960b /cfrontend/C2C.ml | |
| parent | 616f939e3ac7ff052f0eb7bce8c16873730ddf0e (diff) | |
| download | compcert-kvx-2dca62f38463b0ebce24fff50666c846df50488e.tar.gz compcert-kvx-2dca62f38463b0ebce24fff50666c846df50488e.zip | |
attempts at generating builtins, start
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index bd9b7487..1ab38a2b 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -154,6 +154,10 @@ let ais_annot_functions = else [] +let builtin_ternary suffix typ = + ("__builtin_ternary_" ^ suffix), + (typ, [TInt(IInt, []); typ; typ], false);; + let builtins_generic = { Builtins.typedefs = []; Builtins.functions = @@ -180,7 +184,10 @@ let builtins_generic = { TPtr(TVoid [AConst], []); TInt(IULong, []); TInt(IULong, [])], - false); + false); + (* Ternary operator *) + builtin_ternary "uint" (TInt(IUInt, [])); + (* Annotations *) "__builtin_annot", (TVoid [], |