Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Refactored the printing functions a little bit more by moving the system ↵ | Bernhard Schommer | 2014-10-28 | 4 | -328/+397 |
| | | | | dependent parts into other modules and some of the functions into a util file. | ||||
* | Added the type information to the global information stored for each atom. | Bernhard Schommer | 2014-10-27 | 2 | -5/+20 |
| | |||||
* | Merge branch 'master' into dwarf | Bernhard Schommer | 2014-10-27 | 2 | -2/+3 |
|\ | |||||
| * | Tune behavior wrt warnings: | Xavier Leroy | 2014-10-24 | 2 | -2/+3 |
| | | | | | | | | | | | | - cchecklink was compiled with -warn-error, which is bad for production code - silence warning 3 (deprecated functions) - silence warning 20 (unused function argument) for Coq-extracted files. | ||||
* | | Added more functionality to DwarfUtil. | Bernhard Schommer | 2014-10-24 | 1 | -0/+39 |
| | | |||||
* | | Added a file for utility functions on the Dwarf types. | Bernhard Schommer | 2014-10-23 | 2 | -42/+66 |
| | | |||||
* | | Added type for all tags. | Bernhard Schommer | 2014-10-21 | 1 | -1/+22 |
| | | |||||
* | | Fixed smaller mistakes. | Bernhard Schommer | 2014-10-21 | 1 | -8/+7 |
| | | |||||
* | | Removed more not needed attributes. | Bernhard Schommer | 2014-10-20 | 1 | -92/+32 |
| | | |||||
* | | Merge branch 'master' into dwarf | Bernhard Schommer | 2014-10-20 | 1 | -0/+1 |
|\| | |||||
| * | Deactivated the warning for deprecated features for compilation of ↵ | Bernhard Schommer | 2014-10-20 | 1 | -0/+1 |
| | | | | | | | | cchecklink since it breaks the build with newer ocaml versions. | ||||
* | | Removed more not needed attributes from the tag types. | Bernhard Schommer | 2014-10-17 | 1 | -19/+50 |
| | | |||||
* | | Merge branch 'master' into dwarf | Bernhard Schommer | 2014-10-17 | 1 | -1/+0 |
|\| | |||||
| * | Removed duplicated open. | Bernhard Schommer | 2014-10-17 | 1 | -1/+0 |
| | | |||||
* | | Started revising the tag types to only include attributes which are actually ↵ | Bernhard Schommer | 2014-10-15 | 1 | -17/+10 |
| | | | | | | | | used debuggers. | ||||
* | | Added the rest of the type for the tags mentioned in appendix 1 of the dwarf ↵ | Bernhard Schommer | 2014-10-15 | 1 | -1/+56 |
| | | | | | | | | 2 standard. | ||||
* | | Added more types. | Bernhard Schommer | 2014-10-14 | 1 | -0/+125 |
| | | |||||
* | | Added a file containing definitions for the types used to store the debug ↵ | Bernhard Schommer | 2014-10-13 | 2 | -1/+122 |
|/ | | | | information. The types follow the Current Attributes by Tag Value in Appendix 1 of the Dwarf 2 standard. | ||||
* | Revised translation of '&&' and '||' to Clight. | Xavier Leroy | 2014-10-13 | 11 | -124/+109 |
| | | | | | | | | | | | The previous translation (in SimplExpr) produced references to the same temporary variable with two different types (bool and int), which is not nice if we want to typecheck the generated Clight. The new translation avoids this and also gets rid of the double cast to bool then to int. The trick is to change Eparen (in CompCert C expressions) to take two types: the type to which the argument must be converted, and the type with which the resulting expression is seen. | ||||
* | Update Makefile, dependencies, and Changelog after upgrade to Flocq 2.4.0. | Xavier Leroy | 2014-10-09 | 3 | -1/+3 |
| | |||||
* | Merge pull request #1 from jhjourdan/master | Xavier Leroy | 2014-10-09 | 21 | -942/+6030 |
|\ | | | | | Upgrade to flocq 2.4.0 | ||||
| * | Upgrade to flocq 2.4.0 | Jacques-Henri Jourdan | 2014-10-07 | 21 | -942/+6030 |
| | | |||||
* | | Refactored the code of ia32/PrintAsm.ml by moving the functions depending on ↵ | Bernhard Schommer | 2014-10-08 | 1 | -138/+220 |
| | | | | | | | | the target system in a seperate module. | ||||
* | | Refactored the code of powerpc/PrintAsm.ml by moving the function depending ↵ | Bernhard Schommer | 2014-10-08 | 1 | -200/+236 |
|/ | | | | on the target system in a seperate module. | ||||
* | Refactored the code of arm/PrintAsm.ml in order to allow the parametrization ↵ | Bernhard Schommer | 2014-10-06 | 1 | -44/+86 |
| | | | | of the printing code over the configuration-dependent bits. | ||||
* | Removed environment variable for the stdlib_path and added a new variable ↵ | Bernhard Schommer | 2014-10-06 | 3 | -20/+20 |
| | | | | for the configuration file. | ||||
* | Change the way the tools like the linker, assembler, etc. are specified by ↵ | Bernhard Schommer | 2014-09-30 | 4 | -22/+113 |
| | | | | including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start. | ||||
* | Moved the timing facility to a seperate file. | Bernhard Schommer | 2014-09-29 | 5 | -54/+68 |
| | |||||
* | Refactoring in the printing of FP numbers. | Xavier Leroy | 2014-09-24 | 1 | -8/+2 |
| | |||||
* | Add theorem "elements_remove". | Xavier Leroy | 2014-09-24 | 1 | -167/+178 |
| | | | | | Use "elements_remove" to simplify the proof of "cardinal_remove". Simplify some of the proofs over function "xelements". | ||||
* | Upgrade clightgen with the new features of CompCert 2.4 (single floats, etc). | Xavier Leroy | 2014-09-24 | 1 | -7/+20 |
| | |||||
* | GCCism: accept __volatile and __volatile__ | Xavier Leroy | 2014-09-21 | 1 | -0/+2 |
| | | | | | These alternate keywords for "volatile" are used in some header files in the wild. | ||||
* | Add .gitignore files. | Xavier Leroy | 2014-09-21 | 6 | -0/+63 |
| | |||||
* | Error instead of warning on illegal escape sequences. | Xavier Leroy | 2014-09-21 | 2 | -1/+5 |
| | | | | | | | | The previous behavior for illegal escape sequences (e.g. '\%') in character and string literals was to emit an error, then treat "\x" as "x". As reported by a user, this is dangerous, because the warning can go unnoticed, and other compilers can treat "\x" as "\\x" (backslash followed by 'x'). Better to error out. | ||||
* | Trim blank linesv2.4 | xleroy | 2014-09-17 | 1 | -2/+0 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2625 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Update changelog and version for 2.4 | xleroy | 2014-09-17 | 2 | -3/+4 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2624 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Tolerance in parsing of 'section' pragma | xleroy | 2014-09-17 | 1 | -0/+3 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2623 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Cold feet: suppress builtins for load with reservation/store conditional, ↵ | xleroy | 2014-08-28 | 5 | -47/+2 |
| | | | | | | use case is unclear. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Update | xleroy | 2014-08-28 | 1 | -1/+2 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2621 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Update for 2.4 | xleroy | 2014-08-27 | 1 | -23/+37 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2620 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Rename __builtin_cntlz to __builtin_clz. | xleroy | 2014-08-27 | 11 | -6/+25 |
| | | | | | | | IA32: add __builtin_clz, __builtin_ctz. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | More efficient implementations of map, fold, etc. | xleroy | 2014-08-27 | 1 | -164/+109 |
| | | | | | | | (Contributed by Vincent Laporte.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2618 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | More careful detection of inlined builtins. Produces better error messages ↵ | xleroy | 2014-08-25 | 1 | -0/+1 |
| | | | | | | if an unsupported __builtin_xxx function is used by mistake. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2617 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Use VFD regs to implement 64-bit mem-mem copies in builtin_memcpy_false. | xleroy | 2014-08-21 | 3 | -5/+10 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2616 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Support C99 compound literals (by expansion in Unblock pass). | xleroy | 2014-08-21 | 16 | -454/+801 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Follow-up to commit 2613 | xleroy | 2014-08-20 | 1 | -0/+2 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2614 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Add builtins for load with reservation and conditional store. | xleroy | 2014-08-20 | 5 | -1/+39 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2613 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Wrong types for strex builtins. | xleroy | 2014-08-20 | 1 | -4/+4 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2612 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Better validation of target for ARM | xleroy | 2014-08-20 | 1 | -1/+5 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2611 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Obvious typos in commit r2609 | xleroy | 2014-08-20 | 1 | -8/+8 |
| | | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2610 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e |