aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/C.mli
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-04-17 16:30:43 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-04-17 16:30:43 +0200
commit1b5db339bb05f773a6a132be4c0b8cea54d50461 (patch)
tree5c7c767bc107eca66fdf6795777821572c5ec5af /cparser/C.mli
parent3d751c114fe4611a5b72e160127be09cf6c6cfec (diff)
downloadcompcert-kvx-1b5db339bb05f773a6a132be4c0b8cea54d50461.tar.gz
compcert-kvx-1b5db339bb05f773a6a132be4c0b8cea54d50461.zip
Experiment: support a subset of GCC's extended asm statements.
Diffstat (limited to 'cparser/C.mli')
-rw-r--r--cparser/C.mli6
1 files changed, 5 insertions, 1 deletions
diff --git a/cparser/C.mli b/cparser/C.mli
index 71ab1d4d..72e1f787 100644
--- a/cparser/C.mli
+++ b/cparser/C.mli
@@ -190,6 +190,10 @@ and init =
| Init_struct of ident * (field * init) list
| Init_union of ident * field * init
+(** GCC extended asm *)
+
+type asm_operand = string option * string * exp
+
(** Statements *)
type stmt = { sdesc: stmt_desc; sloc: location }
@@ -210,7 +214,7 @@ and stmt_desc =
| Sreturn of exp option
| Sblock of stmt list
| Sdecl of decl
- | Sasm of string
+ | Sasm of attributes * string * asm_operand list * asm_operand list * string list
and slabel =
| Slabel of string