diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-07-21 17:09:45 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-21 17:09:45 +0200 |
| commit | 3a1b0e98a09dd9688e8f45f9677b7ea25f4720bf (patch) | |
| tree | 20a54d4aa45c33de63c8579ada5c56d8883e60de /cparser | |
| parent | 4adf6e3a967055df66fb815c92350dc835bb06dc (diff) | |
| download | compcert-kvx-3a1b0e98a09dd9688e8f45f9677b7ea25f4720bf.tar.gz compcert-kvx-3a1b0e98a09dd9688e8f45f9677b7ea25f4720bf.zip | |
Support __builtin_constant_p as in GCC and Clang (#367)
Returns 1 if the argument is a constant expression, 0 otherwise.
Closes: #366
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Elab.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index b74e34d0..4bd0bdfa 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1809,6 +1809,16 @@ let elab_expr ctx loc env a = (print_typ env) ty (print_typ env) ty' (print_typ env) ty' (print_typ env) ty; { edesc = ECall(ident, [b2; b3]); etyp = ty },env + | CALL(VARIABLE "__builtin_constant_p", al) -> + begin match al with + | [a1] -> + let b1,env = elab env a1 in + let v = if Ceval.is_constant_expr env b1 then 1L else 0L in + intconst v IInt, env + | _ -> + fatal_error "'__builtin_constant_p' expects one argument" + end + | CALL((VARIABLE "__builtin_sel" as a0), al) -> begin match al with | [a1; a2; a3] -> |