aboutsummaryrefslogtreecommitdiffstats
path: root/driver
Commit message (Collapse)AuthorAgeFilesLines
* 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.
| | * | Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-222-11/+13
| | | |
| | * | Introduce symbol environments (type Senv.t) as a restricted view on global ↵Xavier Leroy2014-11-261-1/+1
| | | | | | | | | | | | | | | | environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
* | | | Merge branch 'master' into dwarfBernhard Schommer2015-01-123-30/+38
|\| | | | | | | | | | | | | | | | | | | Conflicts: powerpc/PrintAsm.ml
| * | | PR#16: give option rules precedence over file pattern rules.Xavier Leroy2015-01-033-31/+38
| | | | | | | | | | | | | | | | | | | | | | | | Plus: simplify handling of -help and --help. Plus: error on unrecognized "-xxx" options so that "-foo.c" is not treated as a source file.
| * | | PR#14: recognize ".so" arguments as files to pass to the linker.Xavier Leroy2015-01-021-1/+2
| | |/ | |/|
* | | Merge branch 'master' into dwarfBernhard Schommer2014-12-171-2/+7
|\| | | | | | | | | | | | | | Conflicts: powerpc/PrintAsm.ml
| * | Stdlib path is ignored when the configuration has_runtime_lib is set to false.Bernhard Schommer2014-12-151-2/+7
| | |
* | | Merge branch 'master' into dwarfBernhard Schommer2014-12-041-1/+1
|\| |
| * | Removed unused variable and changed the search for the installation ↵Bernhard Schommer2014-12-041-1/+1
| |/ | | | | | | directory. Use Sys.executable_name instead of Sys.argv.(0).
* / Renamed the printer module for the Abbreviations and deactivated adding the ↵Bernhard Schommer2014-12-021-1/+1
|/ | | | -g option to the assembler.
* Verification of the Unusedglob pass (removal of unreferenced static global ↵Xavier Leroy2014-11-242-2/+9
| | | | definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
generated by cgit (git 2.34.1) at 2024-07-01 07:09:43 +0000