aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Expand)AuthorAgeFilesLines
* Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-151-6/+6
* Code cleanup.Bernhard Schommer2016-03-103-9/+6
* Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-202-4/+8
|\
| * Implemented the usage of DW_AT_ranges for non-contiguous address ranges.Bernhard Schommer2015-10-162-0/+2
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-1414-1666/+1666
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-143-8/+8
| * Changed the type of the debug sections with additional string.Bernhard Schommer2015-10-132-4/+4
| * Implement the usage of the debug_str section for the gcc backend.Bernhard Schommer2015-10-132-2/+4
* | Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-2017-1673/+1673
* | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-114-25/+23
|/
* Filled in the rest of the funciton needed for thte debug info under arm.Bernhard Schommer2015-10-092-0/+2
* Added versions of the tranform_* functions in AST to work with functionsBernhard Schommer2015-10-081-1/+216
* Change the way the debug sections are printed.Bernhard Schommer2015-09-282-2/+2
* Added support for the locations of stack allocated local variables.Bernhard Schommer2015-09-252-0/+2
* Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-223-16/+16
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-213-358/+297
* Represent external worlds by a coinductive type rather than an inductive type.Xavier Leroy2015-06-071-1/+1
* In AST.calling_conventions, record whether the original C function was "old-s...Xavier Leroy2015-05-221-3/+4
* Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-091-2/+2
* Typo: Val.sun_inject -> Val.sub_inject.Xavier Leroy2015-05-061-1/+1
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...Xavier Leroy2015-04-305-111/+113
* Support for GCC-style extended asm, continued:Xavier Leroy2015-04-213-5/+6
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-173-8/+8
* Merge branch 'master' into dwarfBernhard Schommer2015-04-024-46/+249
|\
| * Merge pull request #34 from AbsInt/extended-annotationsXavier Leroy2015-04-014-29/+216
| |\
| | * Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-271-2/+4
| | * Extended arguments to annotations, continued:Xavier Leroy2015-03-272-34/+6
| | * Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-273-29/+242
| * | Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-151-17/+33
| |/
* | Started integrating the debug printing in the common backend_printer.Bernhard Schommer2015-03-112-2/+2
* | Starting to remove the seperate printers for each backend.Bernhard Schommer2015-02-022-0/+4
|/
* 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-234-177/+260
|\
| * 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-262-150/+218
* | Clean up support for common symbols. Uninitialized "const" symbols can be co...Xavier Leroy2014-12-172-8/+8
|/
* Add Genv.public_symbol operation.Xavier Leroy2014-11-244-180/+342
* Record public global definitions via field "prog_public" in AST.program.Xavier Leroy2014-11-241-3/+25
* Excessively strict validation: ofs + sz < modulus should have beenxleroy2014-08-201-4/+5
* Issue with switch labels that are negative 32-bit integers.xleroy2014-08-171-0/+35
* - Support "switch" statements over 64-bit integersxleroy2014-08-172-171/+264
* Add Mem.free_parallel_inject and use it to simplify Events a bit.xleroy2014-07-313-35/+50
* Update "read_as_zeros" property.xleroy2014-07-231-1/+3
* Merge of "newspilling" branch:xleroy2014-07-238-504/+602
* Add "read_as_zero" property for memory areas initialized by Init_space.xleroy2014-06-301-14/+106
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-0/+17
* Merge of branch linear-typing:xleroy2014-04-061-0/+435
* Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):xleroy2014-03-281-435/+0
* Revised division of labor between RTLtyping and Lineartyping:xleroy2014-03-271-0/+435
* Type-checking of builtin volatile write Mfloat32 was too strict, causing type...xleroy2014-03-242-4/+4
generated by cgit (git 2.34.1) at 2024-06-02 16:56:58 +0000