aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| * | Added a phantom parameter to [specifier_qualifier_list].François Pottier2015-10-231-3/+4
| | |
| * | A general comment about phantom parameters.François Pottier2015-10-231-0/+16
| | |
| * | Remove all productions that involve the [error] token.François Pottier2015-10-231-34/+0
| | | | | | | | | | | | | | | These productions were used to give better error messages in some situations. They are no longer useful, since we are building a whole new system for reporting errors.
| * | Added [Cerrors.fatal_error_raw].François Pottier2015-10-232-0/+13
| | |
| * | A .gitignore entry.François Pottier2015-10-231-0/+1
| | |
| * | Read the whole source C file into memory instad of reading it on demand.François Pottier2015-10-232-5/+17
| | | | | | | | | | | | | | | Having the file in memory will help build an error message. Also, this may be slightly faster.
| * | Makefile.extr: [make clean] removes .automaton files.François Pottier2015-10-231-0/+1
| | |
| * | Switch to --table mode. This is slightly slower but otherwise changes nothing.François Pottier2015-10-231-1/+1
| | |
| * | Distinguish [MENHIR] and [MENHIR_MODE]. Cleaner, more flexible.François Pottier2015-10-231-5/+9
| | |
| * | Fix [Lexer.char_literal] and [Lexer.string_literal] to properly keep track ↵François Pottier2015-10-221-10/+12
| | | | | | | | | | | | | | | | | | of [lex_start_p]. This is required for Menhir to pick up the correct start position of the token.
* | | Added additional option for the renaming of the suffix of the sdumpBernhard Schommer2015-10-231-2/+6
| |/ |/| | | | | | | | | | | | | file. The new option -sdump-suffix allows it to specify another suffix for the sdump file. Bug 17326
* | Added special treatment for large stack size for ppc.Bernhard Schommer2015-10-231-3/+3
| | | | | | | | | | | | Since the stacksize is casted to signed int in the alloc frame function large stacksize lead to assembler containing overflows. Bug 17473.
* | Merge branch 'clean' of https://github.com/fpottier/CompCert into fpottier-cleanBernhard Schommer2015-10-203-90/+180
|\| | | | | | | | | Conflicts: Makefile.extr
| * It is probably more efficient to eagerly evaluate $(MENHIR_INCLUDES).François Pottier2015-10-161-1/+1
| | | | | | | | This should save a lot of calls to the shell, menhir, and ocamlfind.
| * Added [Makefile.menhir], which gives a choice between Menhir's "code" and ↵François Pottier2015-10-162-7/+77
| | | | | | | | | | | | | | | | | | | | "table" back-ends when compiling CompCert. For now, MENHIR_TABLE is set to false, so CompCert is not affected. Setting MENHIR_TABLE to true builds CompCert using Menhir's table back-end. This causes a small but repeatable slowdown on "make test", about 2% (roughly 1 second out of 40). I have tested building ccomp and ccomp.byte. I have tested with an ocamlfind-installed menhir and with a manually-installed menhir.
| * Replaced 4 uses of [ioption(declaration_specifiers_no_type)] with ↵François Pottier2015-10-081-4/+4
| | | | | | | | | | | | | | [declaration_specifiers_no_type?]. Inlining these options was not necessary. This reduces the number of states in the automaton.
| * Cosmetic. Removed some spaces. Shared one redundant semantic action {}.François Pottier2015-10-071-7/+6
| |
| * One cosmetic change of [option] to [?]. No impact.François Pottier2015-10-071-1/+1
| |
| * Factorized the two forms of FOR statement by introducing [for_statement_header].François Pottier2015-10-071-2/+6
| | | | | | | | This leads to a smaller automaton.
| * Introduced optional(X, Y), which means X? Y, and used it in array ↵François Pottier2015-10-071-4/+12
| | | | | | | | | | | | declarators and FOR loops. This leads to fewer automaton states, and potentially better error messages.
| * Factorized the productions for several categories of binary operators.François Pottier2015-10-071-13/+20
| | | | | | | | | | | | | | This leads to a small savings in the number of states (which could become greater in the future if we decide to parameterize expressions). If desired, the old automaton could be recovered by marking the binary operators as %inline.
| * Factorized two productions (and two error productions) in [enum_specifier].François Pottier2015-10-071-5/+2
| | | | | | | | This is analogous to the previous commit.
| * Factorized two productions (and two error productions) in ↵François Pottier2015-10-071-5/+2
| | | | | | | | | | | | | | | | | | | | | | [struct_or_union_specifier]. The old version was strictly equivalent to using [ioption(other_identifier)]. The new version uses [option(other_identifier)] instead, that is, [other_identifier?]. Technically, this means that [set_id_type i OtherId] is called slightly earlier (at the opening brace, instead of at the closing brace), but this does not make any difference, since the re-classification of identifiers affects only the second parsing phase.
| * For clarity, removed several redundant calls to [set_id_type].François Pottier2015-10-071-9/+5
| | | | | | | | | | | | | | A TYPEDEF_NAME is already classified as a [TypedefId] by the lexer, and similarly, a VAR_NAME is already classified as a [VarId]. Thus, the removed calls had no effect. The remaining calls to [set_id_type] are useful, as they can re-classify a token.
| * Introduced [other_identifier] as a more elegant way of calling [set_id_type ↵François Pottier2015-10-071-19/+22
| | | | | | | | | | | | i OtherId]. This causes no change in the automaton.
| * One more replacement of [ioption] with [option].François Pottier2015-10-071-1/+1
| | | | | | | | I missed this opportunity in the previous commit.
| * Use [option] as much as possible and [ioption] only where necessary.François Pottier2015-10-071-13/+30
| | | | | | | | | | | | | | | | | | The existing [option(X)] was marked %inline, and has been renamed [ioption(X)]. A new [option(X)], which is not marked %inline, has been introduced. The grammar now uses [option] everywhere, except where [ioption] is necessary in order to avoid conflicts. This reduces the number of states in the automaton. The number of LR(0) cores drops from 857 to 712.
| * Add -la 1 to Menhir's invocation, to see statistics and warnings.François Pottier2015-10-071-1/+1
| |
| * Add whitespace, for better vertical alignment and better readability.François Pottier2015-10-071-21/+13
| | | | | | | | This violates the 80-column width limit, but is really important.
| * Pass --no-stdlib and -v to menhir when compiling pre_parser.mly.François Pottier2015-10-072-1/+2
| | | | | | | | | | | | | | Passing --no-stdlib ensures that there is no dependency on Menhir's standard library. Passing -v, which is equivalent to --explain --dump, requests the generation of pre_parser.automaton, a description of the automaton.
* | Also replace extern_atom by camlstring_of_coqstring for ia32/TargetPrinter.ml.Bernhard Schommer2015-10-201-2/+2
| | | | | | | | Bug 17450
* | Added not merged destruction of Archi. Bug 17450Bernhard Schommer2015-10-201-0/+2
| |
* | Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-2073-7292/+2106
|\ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: arm/TargetPrinter.ml backend/CMparser.mly backend/SelectLongproof.v backend/Selectionproof.v cfrontend/C2C.ml checklink/Asm_printers.ml checklink/Check.ml checklink/Fuzz.ml common/AST.v debug/DebugInformation.ml debug/DebugInit.ml debug/DwarfPrinter.ml debug/DwarfTypes.mli debug/Dwarfgen.ml exportclight/ExportClight.ml ia32/TargetPrinter.ml powerpc/Asm.v powerpc/SelectOpproof.v powerpc/TargetPrinter.ml
| * | Do not dump the .sdump files.Bernhard Schommer2015-10-161-15/+2
| | | | | | | | | | | | Bug 16529.
| * | Fixed typos in the arm and ia32 section printing.Bernhard Schommer2015-10-162-3/+3
| | | | | | | | | | | | Bug 17392
| * | Implemented the usage of DW_AT_ranges for non-contiguous address ranges.Bernhard Schommer2015-10-1612-61/+145
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The gcc produces DW_AT_ranges for non-contiguous address ranges, like compilation units containing functions which are placed in different ELF-sections or lexical scopes that are split up. With this commit CompCert also uses this DWARF v3 feature for gnu backend based targets. In order to ensure backward compability a flag is added which avoids this and produces debug info in DWARF v2 format. Bug 17392.
| * | First step to implemente address ranges for the gnu backend.Bernhard Schommer2015-10-1511-100/+100
| | | | | | | | | | | | | | | | | | | | | | | | | | | In contrast to the dcc, the gcc uses address ranges to express non-contiguous range of addresses. As a first step we set the start and end addresses for the different address ranges for the compilation unit by using the start and end addresses of functions. Bug 17392.
| * | Use section type also for other targets.Bernhard Schommer2015-10-152-4/+4
| | | | | | | | | | | | Bug 17392.
| * | More verbose debug printer.Bernhard Schommer2015-10-144-227/+274
| | | | | | | | | | | | | | | | | | | | | | | | Like, for example the clang, CompCert now prints a more detailed descriptions of the debug information in the assembler file. For each abbreviation and debug entry the dwarf attributes and their encodings are added. Bug 17392.
| * | Reworked the section interface for the debug information.Bernhard Schommer2015-10-144-26/+37
| | | | | | | | | | | | | | | | | | Instead of pushing strings around use the actual section. However the string is still used in the Hashtbl. Bug 17392.
| * | bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-14156-11180/+11180
| | |
| * | bug 17392: fix typo in OS nameMichael Schmidt2015-10-141-1/+1
| | |
| * | bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-1465-530/+530
| | |
| * | Changed the type of the debug sections with additional string.Bernhard Schommer2015-10-134-12/+19
| | | | | | | | | | | | | | | | | | | | | | | | Instead of using a string they now take an optional string, which should be none if the backend is not the diab backend and the corresponding section is the text section and Some s with s being the custom section name else. Bug 17392.
| * | Implement the usage of the debug_str section for the gcc backend.Bernhard Schommer2015-10-139-477/+552
| | | | | | | | | | | | | | | | | | | | | | | | GCC prints all string larger than 3 characters in the debug_str section which reduces the size of the debug information since entries containing the same string now map to the same string in the debug_str sections. Bug 17392.
| * | Remove unused members from debug types.Bernhard Schommer2015-10-133-21/+0
| | | | | | | | | | | | | | | | | | | | | The dwarf 2 standard allows more attributes for certain debuggint entries than used by gcc or diab data. Since they are also not set by compcert they can be removed. Bug 17392.
| * | Removed unused function.Bernhard Schommer2015-10-131-7/+2
| | | | | | | | | | | | | | | The function exists_type is not really used so we can remove it. Bug 17392.
| * | Changed definition of implem for debug information.Bernhard Schommer2015-10-125-173/+135
| | | | | | | | | | | | | | | | | | | | | Instead of making each filed mutuable we use a reference to a record of type implem. Now only the default implementation and the default debug information need to be upated to add a new function. Bug 17392.
| * | Use a more descriptive type for diab debug entries.Bernhard Schommer2015-10-123-13/+25
| | | | | | | | | | | | | | | | | | Instead of using a tuple we now use a record with descriptive names for the different entries. Bug 17392
| * | Move strip functions to Cutil.Bernhard Schommer2015-10-123-41/+47
| | | | | | | | | | | | | | | | | | Since the strip functions might be useful in other context and is more general then the debug information. Bug 17392.
generated by cgit (git 2.34.1) at 2024-07-05 15:24:37 +0000