aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CminorSel.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-6/+6
|\
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-2/+2
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-4/+4
* | __builtin_expect seems to workDavid Monniaux2020-04-071-4/+4
|/
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-061-1/+5
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-11/+11
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-8/+8
* Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-221-2/+2
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-34/+34
* Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-0/+34
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-10/+35
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-1/+1
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-22/+53
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-0/+15
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Merge of the clightgen branch:xleroy2012-12-291-1/+0
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-65/+25
* Merge of the newmem branch:xleroy2012-05-211-4/+12
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-2/+2
* Merge of branch "unsigned-offsets":xleroy2011-04-091-2/+2
* Support for inlined built-ins.xleroy2010-06-291-2/+9
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-1/+1
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-101-1/+1
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-15/+19
* Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...xleroy2009-08-171-0/+122
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-7/+7
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-9/+2
* Cminor, CminorSel: removed useless premises in rules for Sreturnxleroy2009-01-041-2/+0
* Fusion partielle de la branche contsem: xleroy2008-07-081-176/+189
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-281-133/+196
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-0/+296
generated by cgit (git 2.34.1) at 2024-05-09 10:35:41 +0000