aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into struct-passingXavier Leroy2015-03-1434-616/+1614
|\
| * Merge branch 'master' of https://github.com/AbsInt/CompCertXavier Leroy2015-03-071-4/+0
| |\
| | * Removed unused target cleansource.Bernhard Schommer2015-03-051-4/+0
| * | Issue #26: problems with big escape sequences in string/char literals.Xavier Leroy2015-03-071-7/+12
| |/
| * Removed leftover references to recdepend.Xavier Leroy2015-02-281-6/+5
| * Removed the recdepend again and replaced it by a builtin Make function.Bernhard Schommer2015-02-272-214/+6
| * Removed the glob files from doc/ instead of doc/glob/Bernhard Schommer2015-02-261-1/+1
| * Updated the recdepend tool to avoid printing of ./ at the begining and printi...Bernhard Schommer2015-02-252-52/+50
| * Added a small ocamlfile that calls ocamlfind recursivly over a given directory.Bernhard Schommer2015-02-243-5/+218
| * Merge github.com:AbsInt/CompCertBernhard Schommer2015-02-239-334/+430
| |\
| | * Update clightgen with respect to new representation of composites.Xavier Leroy2015-02-203-232/+151
| | * Merge pull request #23 from AbsInt/no-shellXavier Leroy2015-02-206-102/+279
| | |\
| | | * Removed the Unix from the libraries for cchecklink.Bernhard Schommer2015-02-201-2/+3
| | | * Merge branch 'no-shell' of github.com:AbsInt/CompCert into compcert_windowsBernhard Schommer2015-02-195-96/+272
| | | |\
| | | | * Merge branch 'master' into no-shellBernhard Schommer2015-02-1981-2496/+6257
| | | | |\ | | | |_|/ | | |/| |
| | | | * Use Unix.create_process instead of Sys.command (continued).Xavier Leroy2014-12-293-96/+122
| | | | * Use Unix.create_process instead of Sys.command to run external tools.Xavier Leroy2014-12-192-0/+150
| | | * | Merge github.com:AbsInt/CompCert into compcert_windowsBernhard Schommer2015-02-1966-2277/+5719
| | | |\ \ | | | |/ / | | |/| |
| | * | | The parameter should also have the old name.Bernhard Schommer2015-02-191-3/+3
| | | * | Removed the linker flag again.Bernhard Schommer2015-01-202-4/+4
| * | | | Removed the MinGW port.Bernhard Schommer2015-02-191-53/+3
| * | | | Merge github.com:AbsInt/CompCertBernhard Schommer2015-02-1919-15/+935
| |\| | |
| | * | | Added back symbol functions in the different printer, since they are still ne...Bernhard Schommer2015-02-191-3/+10
| | * | | Changed the symbol function back to its old definition.Bernhard Schommer2015-02-191-10/+3
| | * | | C reference implementation of the int64 helper functions.Xavier Leroy2015-02-1418-8/+928
| * | | | Use lcomm instead of .local for Mingw.Bernhard Schommer2015-02-101-2/+2
| * | | | Added new Mingw Printer. Currently the only difference to the Cygwin printer ...Bernhard Schommer2015-02-101-13/+55
| |/ / /
| * | | Interpreter produces more detailed trace, including name of semantic rules used.Xavier Leroy2015-02-083-231/+226
| * | | Changed the print_globaldef function of the powerpc backend to look like the ...Bernhard Schommer2015-01-281-10/+2
* | | | Improve performance and configurability for the StructReturn pass.Xavier Leroy2015-03-146-59/+144
* | | | More interoperability tests.Xavier Leroy2015-01-282-9/+34
* | | | ABI compatibility for struct/union function arguments passed by value.Xavier Leroy2015-01-2712-74/+799
|/ / /
* | | Add weaker variants of theorems find_funct_ptr_exists and find_var_exists.Xavier Leroy2015-01-231-70/+122
* | | Merge branch 'named-structs'Xavier Leroy2015-01-2336-1630/+4023
|\ \ \
| * | | Define a nonnegative integer "rank" for types to support structural induction...Xavier Leroy2015-01-102-22/+120
| * | | Add a type system for CompCert C and type-checking constructor functions.Xavier Leroy2014-12-318-80/+2101
| * | | Represent struct and union types by name instead of by structure.Xavier Leroy2014-12-2223-1320/+1535
| * | | Make small-step semantics more parametric w.r.t. the type of global environme...Xavier Leroy2014-11-262-27/+42
| * | | Introduce symbol environments (type Senv.t) as a restricted view on global en...Xavier Leroy2014-11-269-201/+245
* | | | Delay reads from !Machine.config before it is properly initialized.Xavier Leroy2015-01-228-68/+88
* | | | Merge branch containing changes for windows compile.Bernhard Schommer2015-01-203-8/+15
|\ \ \ \ | | |/ / | |/| |
| * | | Renamed LIB into VLIB to avoid clashes with environment variables.Bernhard Schommer2015-01-201-2/+2
| * | | Replaced 8 spaces by tabs.Bernhard Schommer2015-01-161-1/+1
| * | | Added new target to just remove the cm[iox] files and the build executables.Bernhard Schommer2015-01-161-0/+4
| * | | Added missing $ for build_checklinkBernhard Schommer2015-01-151-2/+2
| * | | Added variable to the Makefile to specify additional linker commands and chan...Bernhard Schommer2015-01-153-6/+9
* | | | Protect against redefinition of the __i64_xxx helper library functions.Xavier Leroy2015-01-206-251/+306
* | | | Follow-up to [5aecefe]: be conservative also in the case of a "common" global...Xavier Leroy2015-01-201-6/+21
|/ / /
* | | More prudent analysis of uninitialized const global variables.Xavier Leroy2015-01-091-3/+6
* | | In -g -S mode, annotate the generated asm file with the C source code in comm...Xavier Leroy2015-01-076-86/+243
generated by cgit (git 2.34.1) at 2024-07-07 17:17:25 +0000