aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Expand)AuthorAgeFilesLines
...
* 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
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-125-23/+16
* Introduce and use the platform-specific Archi module giving:xleroy2014-01-032-26/+26
* Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union).xleroy2013-12-302-21/+111
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-282-26/+44
* Merge of branch value-analysis.xleroy2013-12-203-68/+157
* Revised semantics of external functions, continued:xleroy2013-11-181-3/+10
* Revised modeling of external functions and built-in functions: just axiomatizexleroy2013-11-171-114/+25
* powerpc/: new unary operation "addsymbol"xleroy2013-11-172-18/+28
* Cminor parsing and printing (from Andrew Tolmach)xleroy2013-10-161-4/+4
* Merge of Flocq version 2.2.0.xleroy2013-08-021-5/+0
* Alternate characterization of alignment constraints in memory injection, whic...xleroy2013-07-311-107/+108
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+12
* More accurate model of condition register flags for ARM and IA32.xleroy2013-07-131-0/+12
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-031-0/+12
* Merge of the "princeton" branch:xleroy2013-06-165-613/+689
* Merge of the float32 branch: xleroy2013-05-196-43/+967
* Refactoring: move definition of chunk_of_type to AST.v.xleroy2013-05-061-0/+10
* Coq-defined equality functions for Allocation.xleroy2013-05-011-3/+20
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-4/+4
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-208-70/+741
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-103-22/+22
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in xleroy2013-03-093-51/+79
generated by cgit (git 2.34.1) at 2024-06-01 20:27:43 +0000