| Commit message (Expand) | Author | Age | Files | Lines |
... | |
* | Added versions of the tranform_* functions in AST to work with functions | Bernhard Schommer | 2015-10-08 | 1 | -1/+216 |
* | Change the way the debug sections are printed. | Bernhard Schommer | 2015-09-28 | 2 | -2/+2 |
* | Added support for the locations of stack allocated local variables. | Bernhard Schommer | 2015-09-25 | 2 | -0/+2 |
* | Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong. | Xavier Leroy | 2015-08-22 | 3 | -16/+16 |
* | Refactoring of builtins and annotations in the back-end. | Xavier Leroy | 2015-08-21 | 3 | -358/+297 |
* | Represent external worlds by a coinductive type rather than an inductive type. | Xavier Leroy | 2015-06-07 | 1 | -1/+1 |
* | In AST.calling_conventions, record whether the original C function was "old-s... | Xavier Leroy | 2015-05-22 | 1 | -3/+4 |
* | Extended inline asm: revised treatment of clobbered registers. | Xavier Leroy | 2015-05-09 | 1 | -2/+2 |
* | Typo: Val.sun_inject -> Val.sub_inject. | Xavier Leroy | 2015-05-06 | 1 | -1/+1 |
* | Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va... | Xavier Leroy | 2015-04-30 | 5 | -111/+113 |
* | Support for GCC-style extended asm, continued: | Xavier Leroy | 2015-04-21 | 3 | -5/+6 |
* | Experiment: support a subset of GCC's extended asm statements. | Xavier Leroy | 2015-04-17 | 3 | -8/+8 |
* | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-04-02 | 4 | -46/+249 |
|\ |
|
| * | Merge pull request #34 from AbsInt/extended-annotations | Xavier Leroy | 2015-04-01 | 4 | -29/+216 |
| |\ |
|
| | * | Updated the Caml part. Added some more tests in annot1.c. | Xavier Leroy | 2015-03-27 | 1 | -2/+4 |
| | * | Extended arguments to annotations, continued: | Xavier Leroy | 2015-03-27 | 2 | -34/+6 |
| | * | Extend annotations so that they can keep track of global variables and local ... | Xavier Leroy | 2015-03-27 | 3 | -29/+242 |
| * | | Revised semantics of comparisons between a pointer and 0. | Xavier Leroy | 2015-03-15 | 1 | -17/+33 |
| |/ |
|
* | | Started integrating the debug printing in the common backend_printer. | Bernhard Schommer | 2015-03-11 | 2 | -2/+2 |
* | | Starting to remove the seperate printers for each backend. | Bernhard Schommer | 2015-02-02 | 2 | -0/+4 |
|/ |
|
* | Add weaker variants of theorems find_funct_ptr_exists and find_var_exists. | Xavier Leroy | 2015-01-23 | 1 | -70/+122 |
* | Merge branch 'named-structs' | Xavier Leroy | 2015-01-23 | 4 | -177/+260 |
|\ |
|
| * | Make small-step semantics more parametric w.r.t. the type of global environme... | Xavier Leroy | 2014-11-26 | 2 | -27/+42 |
| * | Introduce symbol environments (type Senv.t) as a restricted view on global en... | Xavier Leroy | 2014-11-26 | 2 | -150/+218 |
* | | Clean up support for common symbols. Uninitialized "const" symbols can be co... | Xavier Leroy | 2014-12-17 | 2 | -8/+8 |
|/ |
|
* | Add Genv.public_symbol operation. | Xavier Leroy | 2014-11-24 | 4 | -180/+342 |
* | Record public global definitions via field "prog_public" in AST.program. | Xavier Leroy | 2014-11-24 | 1 | -3/+25 |
* | Excessively strict validation: ofs + sz < modulus should have been | xleroy | 2014-08-20 | 1 | -4/+5 |
* | Issue with switch labels that are negative 32-bit integers. | xleroy | 2014-08-17 | 1 | -0/+35 |
* | - Support "switch" statements over 64-bit integers | xleroy | 2014-08-17 | 2 | -171/+264 |
* | Add Mem.free_parallel_inject and use it to simplify Events a bit. | xleroy | 2014-07-31 | 3 | -35/+50 |
* | Update "read_as_zeros" property. | xleroy | 2014-07-23 | 1 | -1/+3 |
* | Merge of "newspilling" branch: | xleroy | 2014-07-23 | 8 | -504/+602 |
* | Add "read_as_zero" property for memory areas initialized by Init_space. | xleroy | 2014-06-30 | 1 | -14/+106 |
* | Refactoring: move symbol_offset into Genv. | xleroy | 2014-05-24 | 1 | -0/+17 |
* | Merge of branch linear-typing: | xleroy | 2014-04-06 | 1 | -0/+435 |
* | Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping): | xleroy | 2014-03-28 | 1 | -435/+0 |
* | Revised division of labor between RTLtyping and Lineartyping: | xleroy | 2014-03-27 | 1 | -0/+435 |
* | Type-checking of builtin volatile write Mfloat32 was too strict, causing type... | xleroy | 2014-03-24 | 2 | -4/+4 |
* | - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4. | xleroy | 2014-01-12 | 5 | -23/+16 |
* | Introduce and use the platform-specific Archi module giving: | xleroy | 2014-01-03 | 2 | -26/+26 |
* | Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union). | xleroy | 2013-12-30 | 2 | -21/+111 |
* | Simpler, more robust emulation of calls to variadic functions: | xleroy | 2013-12-28 | 2 | -26/+44 |
* | Merge of branch value-analysis. | xleroy | 2013-12-20 | 3 | -68/+157 |
* | Revised semantics of external functions, continued: | xleroy | 2013-11-18 | 1 | -3/+10 |
* | Revised modeling of external functions and built-in functions: just axiomatize | xleroy | 2013-11-17 | 1 | -114/+25 |
* | powerpc/: new unary operation "addsymbol" | xleroy | 2013-11-17 | 2 | -18/+28 |
* | Cminor parsing and printing (from Andrew Tolmach) | xleroy | 2013-10-16 | 1 | -4/+4 |
* | Merge of Flocq version 2.2.0. | xleroy | 2013-08-02 | 1 | -5/+0 |
* | Alternate characterization of alignment constraints in memory injection, whic... | xleroy | 2013-07-31 | 1 | -107/+108 |