aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Cminorgen.v
Commit message (Expand)AuthorAgeFilesLines
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-3/+3
* Update the proofs of the C front-end to the new linking framework.Xavier Leroy2016-03-061-13/+4
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-4/+4
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-3/+3
* Merge of "newspilling" branch:xleroy2014-07-231-0/+2
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...xleroy2014-04-091-7/+3
* Support "default" cases in the middle of a "switch", not just at the end.xleroy2013-12-211-12/+14
* Merge of branch value-analysis.xleroy2013-12-201-199/+29
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-0/+3
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Merge of the clightgen branch:xleroy2012-12-291-238/+66
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-11/+11
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-42/+0
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-1/+2
* More aggressive 'uncasting' before storing small integersxleroy2012-06-301-15/+16
* Merge of the "volatile" branch:xleroy2012-02-041-34/+55
* Merge of the nonstrict-ops branch:xleroy2012-01-141-80/+225
* Merge of branch "unsigned-offsets":xleroy2011-04-091-1/+1
* Merge of branches/full-expr-4:xleroy2010-08-181-228/+38
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-3/+3
* Strengthen chunktype inference and use it to remove some useless casts.xleroy2010-05-051-9/+42
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-62/+223
* In generated Cminor functions, make sure local variables includexleroy2009-08-201-1/+37
* Transition semantics for Clight and Csharpminorxleroy2009-08-031-19/+96
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-1/+1
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-3/+8
* 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-47/+30
* Documentationxleroy2007-08-051-8/+9
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-137/+84
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...xleroy2007-03-021-2/+4
* Meilleure compilation de la negation booleennexleroy2006-09-191-0/+1
* Simplification de Cminor: les affectations de variables locales ne sontxleroy2006-09-181-2/+2
* Revu traitement des variables globales dans AST.program et dans Globalenvs.xleroy2006-09-051-4/+6
* Revu la repartition des sources Coq en sous-repertoiresxleroy2006-09-041-0/+433
generated by cgit (git 2.34.1) at 2024-05-08 12:35:40 +0000