aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Removed unused sel_target, changed cygwin symbol names and changed the defaul...Bernhard Schommer2015-02-195-7/+11
* Added an elf prefix to all common elf functions in PrintAsmaux.Bernhard Schommer2015-02-185-36/+50
* Changed print_fun/var_info to be functions instead of booleans.Bernhard Schommer2015-02-185-18/+16
* Removed some style issues.Bernhard Schommer2015-02-183-76/+82
* Changed arm backend to the common backend printer.Bernhard Schommer2015-02-097-1194/+1145
* Merge remote-tracking branch 'origin/master' into backend_printerBernhard Schommer2015-02-093-231/+226
|\
| * Interpreter produces more detailed trace, including name of semantic rules used.Xavier Leroy2015-02-083-231/+226
* | Changed the ia32 backend to the new Printer.Bernhard Schommer2015-02-065-1035/+983
* | Changed the ASM printer of the powerpc to the generalized backend.Bernhard Schommer2015-02-055-792/+850
* | Moved more common functions into a seperate file.Bernhard Schommer2015-02-044-137/+69
* | Started moving common backend functions into one file.Bernhard Schommer2015-02-033-84/+114
|/
* Changed the print_globaldef function of the powerpc backend to look like the ...Bernhard Schommer2015-01-281-10/+2
* 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
* | PR#19: there is no reason to reject an empty "switch" statement.Xavier Leroy2015-01-061-2/+0
* | PR#16: give option rules precedence over file pattern rules.Xavier Leroy2015-01-033-31/+38
* | PR#14: recognize ".so" arguments as files to pass to the linker.Xavier Leroy2015-01-021-1/+2
* | PR#15: vararg functions are not eligible for inlining.Xavier Leroy2015-01-021-1/+1
* | Translation of wide string literals.Xavier Leroy2015-01-011-6/+57
* | Wrong handling of block-local function declarations (again)Xavier Leroy2015-01-011-12/+7
* | Revised type compatibility check w.r.t. handling of attributes.Xavier Leroy2015-01-014-49/+93
* | PR#12: regression introduced in commit 2d32afcXavier Leroy2014-12-301-2/+0
* | PR#6: fix handling of wchar_t and assignments from wide string literals.Xavier Leroy2014-12-305-9/+31
* | PR#11: support sizeof(struct {...}) and _Alignof(struct {...})Xavier Leroy2014-12-301-25/+38
* | Improve printing of errors.Xavier Leroy2014-12-301-3/+11
* | PR#10 continued: disambiguate record to avoid OCaml warningXavier Leroy2014-12-301-1/+1
* | PR#10: composite definitions must be maintained in the environment.Xavier Leroy2014-12-301-6/+15
* | cparser/Parser.v is generated.Xavier Leroy2014-12-301-0/+1
* | Recognize more of GCC's alternate keywords (e.g. "__signed").Xavier Leroy2014-12-291-21/+24
* | Support "asm volatile" (closes: PR#5).Xavier Leroy2014-12-292-1/+3
* | One more cleanup in configure.Xavier Leroy2014-12-181-1/+1
* | No longer include a pre-generated Parser.v in the distribution.Xavier Leroy2014-12-184-61679/+15
* | Merge pull request #3 from AbsInt/pure-makefilesXavier Leroy2014-12-188-85/+371
|\ \
| * | Minor bug fixes in configure and Makefile.extrXavier Leroy2014-12-172-5/+6
generated by cgit (git 2.34.1) at 2024-07-02 00:23:04 +0000