From edc00e0c90a5598f653add89f42a095d8ee1b629 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 12 May 2014 15:52:42 +0000 Subject: Assorted fixes to fix parsing issues and be more GCC-like: - Moved scanning of char constants and string literals entirely to Lexer - Parser: separate STRING_LITERAL from CONSTANT to be closer to ISO C99 grammar - pre_parser: adapted + "asm" takes string_literal, not CONSTANT - Revised errors "inline doesnt belong here" git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2492 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cparser/Cabs.v | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'cparser/Cabs.v') diff --git a/cparser/Cabs.v b/cparser/Cabs.v index 23c1cdc5..920f4603 100644 --- a/cparser/Cabs.v +++ b/cparser/Cabs.v @@ -17,7 +17,8 @@ Require Import BinPos. (* OCaml's string type. *) Parameter string : Type. - +(* OCaml's int64 type, used to represent individual characters in literals. *) +Parameter char_code : Type. (* Context information. *) Parameter cabsloc : Type. @@ -140,11 +141,11 @@ with expression := with constant := (* The string is the textual representation of the constant in - the source code. It does include quotes. *) + the source code. *) | CONST_INT : string -> constant | CONST_FLOAT : floatInfo -> constant - | CONST_CHAR : string -> constant - | CONST_STRING : string -> constant + | CONST_CHAR : bool -> list char_code -> constant + | CONST_STRING : bool -> list char_code -> constant with init_expression := | NO_INIT @@ -208,7 +209,7 @@ with statement := | DEFAULT : statement -> cabsloc -> statement | LABEL : string -> statement -> cabsloc -> statement | GOTO : string -> cabsloc -> statement - | ASM : constant -> cabsloc -> statement + | ASM : bool -> list char_code -> cabsloc -> statement | DEFINITION : definition -> statement (*definition or declaration of a variable or type*) with for_clause := -- cgit