aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/Asmgenproof1.v
Commit message (Expand)AuthorAgeFilesLines
* Remove some useless "Require".xleroy2012-12-301-1/+0
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-1/+9
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-091-1/+1
* Merge of the nonstrict-ops branch:xleroy2012-01-141-275/+446
* Cleaned up old commented-out partsxleroy2011-08-191-24/+0
* More careful treatment of 'load immediate 0' as 'xor self'xleroy2011-08-181-22/+4
* Locations.v: add Loc.diff_dec.xleroy2011-08-141-101/+78
* IA32 port: more faithful treatment of pseudoregister ST0.xleroy2011-08-081-11/+46
* Cleaned up handling of composite conditionsxleroy2011-08-051-24/+110
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-3/+37
* Renamed Machconcr into Machsem.xleroy2011-04-091-5/+5
* Merge of branch "unsigned-offsets":xleroy2011-04-091-50/+55
* Improvements for int8 and int16 storesxleroy2010-09-101-6/+38
* Merge of the reuse-temps branch:xleroy2010-09-021-0/+1436