aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Cabs.v
diff options
context:
space:
mode:
Diffstat (limited to 'cparser/Cabs.v')
-rw-r--r--cparser/Cabs.v8
1 files changed, 7 insertions, 1 deletions
diff --git a/cparser/Cabs.v b/cparser/Cabs.v
index 920f4603..6d9e95d5 100644
--- a/cparser/Cabs.v
+++ b/cparser/Cabs.v
@@ -180,6 +180,12 @@ Definition init_name_group := (list spec_elem * list init_name)%type.
(* e.g.: int x, y; *)
Definition name_group := (list spec_elem * list name)%type.
+(* GCC extended asm *)
+Inductive asm_operand :=
+| ASMOPERAND: option string -> bool -> list char_code -> expression -> asm_operand.
+
+Definition asm_flag := (bool * list char_code)%type.
+
(*
** Declaration definition (at toplevel)
*)
@@ -209,7 +215,7 @@ with statement :=
| DEFAULT : statement -> cabsloc -> statement
| LABEL : string -> statement -> cabsloc -> statement
| GOTO : string -> cabsloc -> statement
- | ASM : bool -> list char_code -> cabsloc -> statement
+ | ASM : list cvspec -> bool -> list char_code -> list asm_operand -> list asm_operand -> list asm_flag -> cabsloc -> statement
| DEFINITION : definition -> statement (*definition or declaration of a variable or type*)
with for_clause :=