aboutsummaryrefslogtreecommitdiffstats
path: root/driver
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-202-16/+10
|\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * Implemented the usage of DW_AT_ranges for non-contiguous address ranges.Bernhard Schommer2015-10-162-1/+8
| | | | | | | | | | | | | | | | | | | | 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.
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-142-36/+36
| |
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-145-18/+18
| |
* | Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-207-54/+54
| |
* | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-3/+3
|/ | | | | | | | | | The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables.
* Push the linker args separate.Bernhard Schommer2015-10-061-2/+4
|
* More refactoring of the Debug Information.Bernhard Schommer2015-09-271-1/+1
| | | | | | | In order to remove unnecessary dependecies the implemenation type is made and the DebugInit file initializes the fields in the record. This allows it to move more functions behind the Debug interface without introducing circular dependencies.
* Move more functionality in the new interface.Bernhard Schommer2015-09-161-4/+5
| | | | | | Added functions to add more information to the debuging interface, like the struct layout with offsets, bitifiled layout and removed the no longer needed mapping from stamp to atom.
* Add the debug interface file.Bernhard Schommer2015-09-161-0/+1
| | | | | | | | The new file Debug.ml contains the interface for generating and printing debug information. In order to generate debug information the init function initializes the necessary functions depending on the -g flag. If the -g is not there all functions are dummy functions which do nothing.
* Merge branch 'new-builtins'Bernhard Schommer2015-09-013-3/+14
|\
| * Improve error reporting in Asmexpand.Xavier Leroy2015-08-241-2/+4
| |
| * Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-232-1/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | SimplLocals: - record locations of stack-allocated variables with annotations (of kind 5) at the beginning of the function; - mark every assignment to non-stack-allocated variables with an annotation of kind 2. Debugvar: (new pass!) - perform availability analysis for debug annotations of kind 2 - insert "start of live range" and "end of live range" annotations (kind 3 and 4) to delimit intervals of PCs where the location of a local variable is known.
* | Improve printing of internal compiler errors.Xavier Leroy2015-08-251-2/+2
| |
* | Fixed the -T option.Bernhard Schommer2015-08-251-1/+1
| | | | | | | | The diab compiler expected -Wm<pathname> without whitespace.
* | Count number of input files and do not use number of source files for ↵Bernhard Schommer2015-08-241-12/+14
| | | | | | | | warning about no input.
* | Added error message when no input file is specified.Bernhard Schommer2015-08-231-0/+5
| |
* | Added the directory ../share/compcert to the search path for .ini files and ↵Bernhard Schommer2015-08-231-9/+12
|/ | | | replaced the if else for the different possibilities by a List.find.
* Added command line option to specify a linker command file for the linker.Bernhard Schommer2015-08-201-0/+5
|
* Also print the system in the output to differentiate between diab and gcc ↵Bernhard Schommer2015-08-051-2/+2
| | | | produced code in later checks.
* Diab defines w_char to be unsigned short.Bernhard Schommer2015-07-071-1/+3
|
* Merge branch 'master' into json_exportBernhard Schommer2015-07-063-13/+23
|\ | | | | | | | | Conflicts: driver/Driver.ml
| * Added Build, Tag, etc in version string and driver/Version.ml should be ignoredBernhard Schommer2015-07-011-1/+1
| |
| * Removed the version from the compcert.ini file and add it again in a ↵Bernhard Schommer2015-07-013-5/+5
| | | | | | | | separate file.
| * Added --version option to print version string.Bernhard Schommer2015-06-261-9/+19
| |
* | Merge branch 'master' into json_exportBernhard Schommer2015-06-174-3/+12
|\|
| * Merge pull request #43 from AbsInt/standard-headersXavier Leroy2015-06-083-2/+9
| |\ | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge of the "standard-headers" branch. This provides CompCert-compatible implementations of the following standard headers: float.h, stdarg.h, stdbool.h, stddef.h, varargs.h. These are the headers that are provided by GCC, Clang, and TCC. Other standard headers are provided by Glibc and similar C standard libraries. So far in CompCert we rely on the headers provided by whatever C compiler is installed on the host platform. This causes some difficulties that this branch addresses: 1- Diab C's stdarg.h is not compatible with CompCert 2- On IA32 and PowerPC, CompCert's "long double" type differs from the "long double" type specified by the ABI. Hence, the platform's float.h gives "long double" parameters that do not match CompCert.
| | * Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-253-2/+9
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This branch provides implementations of the following standard headers: <float.h> <stdarg.h> <stdbool.h> <stddef.h> <varargs.h> These are the headers that are provided by GCC and Clang, as opposed to being provided by Glibc and similar C standard libraries. Configuration flag "-no-standard-headers" deactivates the installation and use of these headers. Lightly tested so far (IA32 Linux).
| * | Represent external worlds by a coinductive type rather than an inductive type.Xavier Leroy2015-06-071-1/+1
| | | | | | | | | | | | As noticed by R. Krebbers, an inductive type for external worlds implies that all sequences of program-world interactions are finite, which is not the case.
| * | Allow the option -o to be also the prefix of the file name for compability ↵Bernhard Schommer2015-05-311-0/+2
| |/ | | | | | | with different build systems.
* | Added flag for the renaming of static functions.Bernhard Schommer2015-05-192-0/+3
| |
* | Moved the information needed from the atoms to the ASM printer and removed ↵Bernhard Schommer2015-05-061-2/+2
| | | | | | | | unused information from the json dump.
* | Added the first version of the sdump export to json.Bernhard Schommer2015-04-271-2/+14
|/
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-171-1/+1
|
* Merge branch 'master' into dwarfBernhard Schommer2015-03-314-2/+116
|\ | | | | | | | | | | Conflicts: Makefile driver/Driver.ml
| * Improvements in the StructReturn transformation (ABI conformance for passing ↵Xavier Leroy2015-03-205-19/+96
| | | | | | | | | | | | | | | | composites). - Implement the "1/2/4/8" composite return policy, used by IA32/MacOS X and IA32/BSD. - Move the default passing conventions from Machine.ml to compcert.ini, making it easier to test the various conventions. - More comprehensive interoperability test in regression/interop1.c.
| * Merge branch 'master' into struct-passingXavier Leroy2015-03-143-189/+180
| |\
| * | Improve performance and configurability for the StructReturn pass.Xavier Leroy2015-03-142-3/+29
| | | | | | | | | | | | | | | | | | | | | | | | configure: special ABI value for IA32/MacOSX and PowerPC/Linux cparser/Machine: special config for PowerPC/Linux cparser/StructReturn: generate better code for return-as-int driver/Clflags, driver/Driver: add options -fstruct-return=<convention> and -fstruct-passing=<convention> to simplify testing
| * | ABI compatibility for struct/union function arguments passed by value.Xavier Leroy2015-01-272-1/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The passing of struct/union arguments by value implemented in the verified part of CompCert is not compatible with the ARM, PowerPC and x86 ABI. Here we enrich the StructReturn source-to-source emulation pass so that it implements the calling conventions defined in these ABIs. Plus: for x86, implement the returning of struct/union results by value in a way compatible with the ABI.
* | | Added missing functions for printing the structs and unions. Still missing ↵Bernhard Schommer2015-03-241-8/+4
| | | | | | | | | | | | printing of packed structs.
* | | Activating the printing of the debug information for supported architecture.Bernhard Schommer2015-03-191-6/+10
| | |
* | | Added function to convert C types into their dwarf represnation.Bernhard Schommer2015-03-181-2/+3
| | |
* | | Started implementing the printing functions for the debug info. Added a ↵Bernhard Schommer2015-03-161-0/+6
| | | | | | | | | | | | global target dependend option to activate the printing only for targets wher it works.
* | | Merge branch 'master' into dwarfBernhard Schommer2015-03-103-189/+180
|\ \ \ | | |/ | |/|
| * | Merge branch 'master' into no-shellBernhard Schommer2015-02-194-137/+113
| |\ \
| | * | Interpreter produces more detailed trace, including name of semantic rules used.Xavier Leroy2015-02-081-95/+61
| | |/ | | | | | | | | | | | | | | | Cexec: record names of rules used in every reduction. Interp: print these rule names in -trace mode. Also: simplified the exploration in "-all" mode; give unique names to states. Csem: fix name of reduction rule "red_call".
| * | Use Unix.create_process instead of Sys.command (continued).Xavier Leroy2014-12-292-94/+119
| | |
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-232-12/+14
|\ \ \ | | |/ | |/|
| * | Merge branch 'named-structs'Xavier Leroy2015-01-232-12/+14
| |\ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Switch CompCert C / Clight AST of composite types (structs and unions) from a structural representation to a nominal representation, closer to concrete syntax. - This avoids algorithmic inefficiencies due to the structural representation. - Closes PR#4. - Smallstep: make small-step semantics more polymorphic in the type of the global environment. - Globalenvs: introduce Senv.t (symbol environments) as a restricted view on Genv.t (full global environments). - Events, Smallstep: use Senv instead of Genv to talk about global names.
generated by cgit (git 2.34.1) at 2024-06-29 04:55:10 +0000