From b960c83725d7e185ac5c6e3c0d6043c7dcd2f556 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Sun, 1 Nov 2015 22:32:23 +0100 Subject: 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 --- cparser/Cabs.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'cparser/Cabs.v') 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 -- cgit