| Commit message (Expand) | Author | Age | Files | Lines |
|---|
| * | ValueAnalysis: use ZTrees instead of ZMaps for abstracting contents of memory... | Xavier Leroy | 2016-05-07 | 1 | -0/+80 |
| * | Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a... | Xavier Leroy | 2016-04-27 | 1 | -0/+244 |
| * | Merge pull request #92 from AbsInt/cleanup | Xavier Leroy | 2016-03-21 | 4 | -8/+18 |
| |\ |
|
| | * | Merge branch 'master' into cleanup | Bernhard Schommer | 2016-03-21 | 2 | -34/+189 |
| | |\ |
|
| | * | | Cleanup of AsmToJSON. | Bernhard Schommer | 2016-03-16 | 1 | -2/+10 |
| | * | | Upgrade ocaml version needed and enable more warnings. | Bernhard Schommer | 2016-03-10 | 2 | -6/+6 |
| | * | | Code cleanup. | Bernhard Schommer | 2016-03-10 | 1 | -0/+2 |
| * | | | Also ignore windows line endings. | Bernhard Schommer | 2016-03-21 | 1 | -1/+2 |
| | |/
|/| |
|
| * | | Preliminaries: extend the Coqlib and Maps libraries. | Xavier Leroy | 2016-03-06 | 2 | -34/+189 |
| |/ |
|
| * | Added printer for Configuration and finished Clflags. | Bernhard Schommer | 2016-01-25 | 1 | -0/+9 |
| * | Started implementing a printer for Clflags. | Bernhard Schommer | 2016-01-25 | 1 | -0/+33 |
| * | Open files in binary mode. | Bernhard Schommer | 2015-11-30 | 1 | -2/+1 |
| * | Updated PR by removing whitespaces. Bug 17450. | Bernhard Schommer | 2015-10-20 | 18 | -1698/+1698 |
| * | Move more functionality in the new interface. | Bernhard Schommer | 2015-09-16 | 1 | -9/+1 |
| * | Added symbol functions for printing of the location for global variables. | Bernhard Schommer | 2015-08-21 | 1 | -0/+7 |
| * | Tighten and prove correct the underflow/overflow bounds for parsing of FP lit... | Xavier Leroy | 2015-07-06 | 2 | -96/+220 |
| * | Give a name to the type of atoms. | Xavier Leroy | 2015-04-23 | 1 | -2/+4 |
| * | remove not used hypotheses in TREE | Jacques-Henri Jourdan | 2015-03-25 | 1 | -9/+4 |
| * | Merge branch 'master' into no-shell | Bernhard Schommer | 2015-02-19 | 2 | -0/+139 |
| |\ |
|
| | * | In -g -S mode, annotate the generated asm file with the C source code in comm... | Xavier Leroy | 2015-01-07 | 2 | -0/+139 |
| * | | Use Unix.create_process instead of Sys.command to run external tools. | Xavier Leroy | 2014-12-19 | 2 | -0/+150 |
| |/ |
|
| * | build_from_parsed: simplified code + correctness proof. | Xavier Leroy | 2014-11-15 | 1 | -15/+86 |
| * | Upgrade to flocq 2.4.0 | Jacques-Henri Jourdan | 2014-10-07 | 2 | -292/+106 |
| * | Add theorem "elements_remove". | Xavier Leroy | 2014-09-24 | 1 | -167/+178 |
| * | More efficient implementations of map, fold, etc. | xleroy | 2014-08-27 | 1 | -164/+109 |
| * | The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM. | xleroy | 2014-07-28 | 1 | -73/+18 |
| * | Merge of "newspilling" branch: | xleroy | 2014-07-23 | 3 | -1468/+2529 |
| * | Tweaks to support defunctorization. | xleroy | 2014-07-23 | 1 | -9/+19 |
| * | Add Proof keyword so that documentation generation works | jjourdan | 2014-07-04 | 1 | -0/+2 |
| * | Cleaner, more resilient parsing of pragmas. | xleroy | 2014-06-05 | 2 | -0/+78 |
| * | Integration of Jacques-Henri Jourdan's verified parser. | xleroy | 2014-04-29 | 1 | -0/+50 |
| * | Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove... | xleroy | 2014-04-09 | 1 | -0/+10 |
| * | Merge of branch linear-typing: | xleroy | 2014-04-06 | 1 | -66/+0 |
| * | floatoflong_from_words, floatoflongu_from_words : proof of PowerPc implementa... | jjourdan | 2014-03-13 | 1 | -89/+316 |
| * | floatoflong_decomp, floatoflongu_decomp | jjourdan | 2014-03-11 | 1 | -0/+238 |
| * | Silence the warning "Cannot build inversion information". | xleroy | 2014-02-24 | 1 | -9/+10 |
| * | Introduce and use the platform-specific Archi module giving: | xleroy | 2014-01-03 | 1 | -7/+6 |
| * | Merge of branch value-analysis. | xleroy | 2013-12-20 | 4 | -53/+615 |
| * | Axioms: remove prop_ext, currently unused AND unsound in Coq 8.4. | xleroy | 2013-12-15 | 1 | -23/+17 |
| * | Merge of the "alignas" branch. | xleroy | 2013-10-05 | 1 | -0/+55 |
| * | Slightly more efficient conversion positive <-> int | xleroy | 2013-09-26 | 1 | -17/+22 |
| * | Small improvements in compilation times for the register allocation pass. | xleroy | 2013-09-20 | 2 | -1/+60 |
| * | Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms | xleroy | 2013-09-14 | 1 | -21/+119 |
| * | Simplify LPMap by smashing bottoms. | xleroy | 2013-08-12 | 1 | -138/+40 |
| * | Merge of Flocq version 2.2.0. | xleroy | 2013-08-02 | 1 | -105/+339 |
| * | Optimize integer divisions by positive constants, turning them into | xleroy | 2013-07-29 | 1 | -0/+28 |
| * | Add another expansion of shrx in terms of shifts and adds (from Hacker's Deli... | xleroy | 2013-07-28 | 1 | -42/+72 |
| * | More properties about subtraction and borrow. | xleroy | 2013-07-15 | 1 | -18/+59 |
| * | More accurate model of condition register flags for ARM and IA32. | xleroy | 2013-07-13 | 2 | -8/+125 |
| * | Revised handling of int->float conversions: | xleroy | 2013-07-08 | 1 | -3/+81 |
