diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-09-14 10:36:25 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-09-14 10:36:25 +0000 |
| commit | 9a0ff6bb768cb0a6e45c1c75727d1cd8199cb89e (patch) | |
| tree | 18a490a5d3573c26d33f1221cb9c771bd290e12c /extraction | |
| parent | 7da3ab1d22658e0328cc26ef595438905e8124d5 (diff) | |
Change the way arguments to __builtin_annot are converted. Use the same conventions as other variadic functions such as printf().
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2325 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'extraction')
0 files changed, 0 insertions, 0 deletions