diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2015-11-12 17:35:41 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2015-11-12 17:35:41 +0100 |
| commit | d90ba4443294b80bd940daedfdcdc3d4334fdc7c (patch) | |
| tree | d647ca2216c342c433c35783d32e1abe8545a72c /cparser/Cabs.v | |
| parent | 9054efbd25eedd5627b9e6e62bf1204e5fa0ae94 (diff) | |
| parent | 0ebefc1d145f82783829174bad1f41bb319742b4 (diff) | |
| download | compcert-d90ba4443294b80bd940daedfdcdc3d4334fdc7c.tar.gz compcert-d90ba4443294b80bd940daedfdcdc3d4334fdc7c.zip | |
Merge pull request #69 from jhjourdan/parser_fix
Parser : duplicate identifier tokens, fix K&R definition parsing
Diffstat (limited to 'cparser/Cabs.v')
| -rw-r--r-- | cparser/Cabs.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cparser/Cabs.v b/cparser/Cabs.v index e15f8694..f5cab15a 100644 --- a/cparser/Cabs.v +++ b/cparser/Cabs.v @@ -81,6 +81,7 @@ with decl_type := | PTR : list cvspec -> decl_type -> decl_type (* The bool is true for variable length parameters. *) | PROTO : decl_type -> list parameter * bool -> decl_type + | PROTO_OLD : decl_type -> list string -> decl_type with parameter := | PARAM : list spec_elem -> option string -> decl_type -> list attribute -> cabsloc -> parameter @@ -190,8 +191,7 @@ Definition asm_flag := (bool * list char_code)%type. ** Declaration definition (at toplevel) *) Inductive definition := - | FUNDEF : list spec_elem -> name -> statement -> cabsloc -> definition - | KRFUNDEF : list spec_elem -> name -> list string -> list definition -> statement -> cabsloc -> definition + | FUNDEF : list spec_elem -> name -> list definition -> statement -> cabsloc -> definition | DECDEF : init_name_group -> cabsloc -> definition (* global variable(s), or function prototype *) | PRAGMA : string -> cabsloc -> definition |