diff options
| author | Michael Schmidt <github@mschmidt.me> | 2023-01-13 12:27:36 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2023-01-23 18:18:21 +0100 |
| commit | 856da72d4190b42a012043a745dddc07a36c60c0 (patch) | |
| tree | 91bf461b1429108de05663cf3cdcca7afad58c28 | |
| parent | 3ebc2e9bd947aa213f2bc5eaf19fe9ffc8f9b5ca (diff) | |
| download | compcert-856da72d4190b42a012043a745dddc07a36c60c0.tar.gz compcert-856da72d4190b42a012043a745dddc07a36c60c0.zip | |
Don't discard argument of `__builtin_va_end`
Instead, evaluate it for the side effects it may contain.
Fixes: #474
| -rw-r--r-- | cfrontend/C2C.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index a23c3cdc..e709c082 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -930,8 +930,8 @@ let rec convertExpr env e = | C.ECall({edesc = C.EVar {name = "__builtin_va_arg"}}, [arg1; arg2]) -> make_builtin_va_arg env (convertTyp env e.etyp) (convertExpr env arg1) - | C.ECall({edesc = C.EVar {name = "__builtin_va_end"}}, _) -> - Ecast (ezero, Tvoid) + | C.ECall({edesc = C.EVar {name = "__builtin_va_end"}}, [arg]) -> + Ecast (convertExpr env arg, Tvoid) | C.ECall({edesc = C.EVar {name = "__builtin_va_copy"}}, [arg1; arg2]) -> let dst = convertExpr env arg1 in |