aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* More functionality for the Printer.Bernhard Schommer2014-11-141-1/+4
|
* Moved abbreviation printer into a seperate file. The printer should also ↵Bernhard Schommer2014-11-123-325/+394
| | | | print the debug info.
* Added functions for printing of the abbreviations.Bernhard Schommer2014-11-113-3/+41
|
* Generalised functionality for the printing of the abbreviations.Bernhard Schommer2014-11-112-235/+307
|
* Added more functions to print the abbreviations.Bernhard Schommer2014-11-062-99/+167
|
* More functions for printing the abbreviations.Bernhard Schommer2014-10-312-77/+141
|
* Reverted changes to C2C since the information needed should be stored ↵Bernhard Schommer2014-10-301-16/+4
| | | | already earlier.
* Started implementing functions to compute the abbreviations for the diab ↵Bernhard Schommer2014-10-292-13/+87
| | | | compiler.
* Refactored the printing functions a little bit more by moving the system ↵Bernhard Schommer2014-10-284-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 Schommer2014-10-272-5/+20
|
* Merge branch 'master' into dwarfBernhard Schommer2014-10-272-2/+3
|\
| * Tune behavior wrt warnings:Xavier Leroy2014-10-242-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 Schommer2014-10-241-0/+39
| |
* | Added a file for utility functions on the Dwarf types.Bernhard Schommer2014-10-232-42/+66
| |
* | Added type for all tags.Bernhard Schommer2014-10-211-1/+22
| |
* | Fixed smaller mistakes.Bernhard Schommer2014-10-211-8/+7
| |
* | Removed more not needed attributes.Bernhard Schommer2014-10-201-92/+32
| |
* | Merge branch 'master' into dwarfBernhard Schommer2014-10-201-0/+1
|\|
| * Deactivated the warning for deprecated features for compilation of ↵Bernhard Schommer2014-10-201-0/+1
| | | | | | | | cchecklink since it breaks the build with newer ocaml versions.
* | Removed more not needed attributes from the tag types.Bernhard Schommer2014-10-171-19/+50
| |
* | Merge branch 'master' into dwarfBernhard Schommer2014-10-171-1/+0
|\|
| * Removed duplicated open.Bernhard Schommer2014-10-171-1/+0
| |
* | Started revising the tag types to only include attributes which are actually ↵Bernhard Schommer2014-10-151-17/+10
| | | | | | | | used debuggers.
* | Added the rest of the type for the tags mentioned in appendix 1 of the dwarf ↵Bernhard Schommer2014-10-151-1/+56
| | | | | | | | 2 standard.
* | Added more types.Bernhard Schommer2014-10-141-0/+125
| |
* | Added a file containing definitions for the types used to store the debug ↵Bernhard Schommer2014-10-132-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 Leroy2014-10-1311-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 Leroy2014-10-093-1/+3
|
* Merge pull request #1 from jhjourdan/masterXavier Leroy2014-10-0921-942/+6030
|\ | | | | Upgrade to flocq 2.4.0
| * Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-0721-942/+6030
| |
* | Refactored the code of ia32/PrintAsm.ml by moving the functions depending on ↵Bernhard Schommer2014-10-081-138/+220
| | | | | | | | the target system in a seperate module.
* | Refactored the code of powerpc/PrintAsm.ml by moving the function depending ↵Bernhard Schommer2014-10-081-200/+236
|/ | | | on the target system in a seperate module.
* Refactored the code of arm/PrintAsm.ml in order to allow the parametrization ↵Bernhard Schommer2014-10-061-44/+86
| | | | of the printing code over the configuration-dependent bits.
* Removed environment variable for the stdlib_path and added a new variable ↵Bernhard Schommer2014-10-063-20/+20
| | | | for the configuration file.
* Change the way the tools like the linker, assembler, etc. are specified by ↵Bernhard Schommer2014-09-304-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 Schommer2014-09-295-54/+68
|
* Refactoring in the printing of FP numbers.Xavier Leroy2014-09-241-8/+2
|
* Add theorem "elements_remove".Xavier Leroy2014-09-241-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 Leroy2014-09-241-7/+20
|
* GCCism: accept __volatile and __volatile__Xavier Leroy2014-09-211-0/+2
| | | | | These alternate keywords for "volatile" are used in some header files in the wild.
* Add .gitignore files.Xavier Leroy2014-09-216-0/+63
|
* Error instead of warning on illegal escape sequences.Xavier Leroy2014-09-212-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.4xleroy2014-09-171-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.4xleroy2014-09-172-3/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2624 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Tolerance in parsing of 'section' pragmaxleroy2014-09-171-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, ↵xleroy2014-08-285-47/+2
| | | | | | use case is unclear. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updatexleroy2014-08-281-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2621 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for 2.4xleroy2014-08-271-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.xleroy2014-08-2711-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.xleroy2014-08-271-164/+109
| | | | | | | (Contributed by Vincent Laporte.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2618 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-08 16:33:45 +0000