diff options
| author | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2015-11-01 22:32:23 +0100 |
|---|---|---|
| committer | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2015-11-01 22:32:23 +0100 |
| commit | b960c83725d7e185ac5c6e3c0d6043c7dcd2f556 (patch) | |
| tree | e4567cd598d32114a440102397c41731f5a65412 /cparser/Cabs.v | |
| parent | e18d267e6912e18462472687abc014a3d04b9a37 (diff) | |
| download | compcert-kvx-b960c83725d7e185ac5c6e3c0d6043c7dcd2f556.tar.gz compcert-kvx-b960c83725d7e185ac5c6e3c0d6043c7dcd2f556.zip | |
Better handling of old-style K&R function declarations:
- Added a Cabs.PROTO_OLD constructor to Cabs.decl_type
- Refactored the Parser.vy and pre_parser.mly grammars
- Rewritten the conversion of old function definitions to new-style
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 6d9e95d5..ab53a3a8 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 |