diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-04-21 13:37:08 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-04-21 13:37:08 +0200 |
commit | c20644efdb39d62a225914636fb4e7816709ad9a (patch) | |
tree | 41e2ed9bbbada3b1feb17df5f5ed989ed7f18124 | |
parent | 656525453ed4aea2a273f0d7503e4610741b6171 (diff) | |
download | compcert-c20644efdb39d62a225914636fb4e7816709ad9a.tar.gz compcert-c20644efdb39d62a225914636fb4e7816709ad9a.zip |
Avoid multiple errors being reported in the case #outputs >= 2.
-rw-r--r-- | cparser/ExtendedAsm.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml index 4cd5fc21..76e368e1 100644 --- a/cparser/ExtendedAsm.ml +++ b/cparser/ExtendedAsm.ml @@ -136,10 +136,14 @@ let transf_outputs loc env = function formatloc loc cstr; (None, [], set_label_reg lbl 0 0 StringMap.empty, 1, 1) end - | _ -> + | outputs -> error "%aUnsupported feature: asm statement with 2 or more outputs" formatloc loc; - (None, [], StringMap.empty, 0, 0) + let rec bind_outputs pos subst = function + | [] -> (None, [], subst, pos, pos) + | (lbl, cstr, e) :: outputs -> + bind_outputs (pos + 1) (set_label_reg lbl pos pos subst) outputs + in bind_outputs 0 StringMap.empty outputs (* Check the clobber list *) |