aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Expand)AuthorAgeFilesLines
* Formatted json printing.Bernhard Schommer2017-06-281-22/+32
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-035-70/+230
* RISC-V port and assorted changesXavier Leroy2017-04-282-3/+25
* Adapt proofs to future handling of literal constants in Coq.Guillaume Melquiond2017-03-081-5/+2
* Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-132-6/+4
* Use "Local" as prefixXavier Leroy2017-02-131-1/+1
* Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.vXavier Leroy2016-12-261-0/+167
* C2C: revise typing and translation of __builtin_memcpy_alignedXavier Leroy2016-11-171-0/+6
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-021-1/+108
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-0/+37
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-3/+454
* IA32: model integer division and modulus closer to the machineXavier Leroy2016-09-181-0/+92
* Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpyXavier Leroy2016-09-171-0/+28
* Decidableplus: remove stuff that was cut-and-paste from Coq 8.5 libraryXavier Leroy2016-09-171-48/+1
* Removed some implict arguments.Bernhard Schommer2016-09-051-5/+3
* Moved quoting functions in ResponsefileBernhard Schommer2016-08-162-2/+36
* Added simplified reader and printer for gnu @filesBernhard Schommer2016-07-203-134/+98
* Added heuristic for passing arg via responsefiles.Bernhard Schommer2016-07-122-20/+0
* Really added the function. Bug 18308Bernhard Schommer2016-07-112-3/+19
* Added function to write responsefiles.Bernhard Schommer2016-07-111-0/+24
* Merge branch 'master' into add-fileBernhard Schommer2016-07-1110-173/+156
|\
| * Port to Coq 8.5pl2Xavier Leroy2016-07-0810-173/+156
* | Added responsefile support for commandline.Bernhard Schommer2016-07-081-0/+133
|/
* Remove code that will is deprecated in ocaml 4.03Bernhard Schommer2016-06-211-0/+10
* ValueAnalysis: use ZTrees instead of ZMaps for abstracting contents of memory...Xavier Leroy2016-05-071-0/+80
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-271-0/+244
* Merge pull request #92 from AbsInt/cleanupXavier Leroy2016-03-214-8/+18
|\
| * Merge branch 'master' into cleanupBernhard Schommer2016-03-212-34/+189
| |\
| * | Cleanup of AsmToJSON.Bernhard Schommer2016-03-161-2/+10
| * | Upgrade ocaml version needed and enable more warnings.Bernhard Schommer2016-03-102-6/+6
| * | Code cleanup.Bernhard Schommer2016-03-101-0/+2
* | | Also ignore windows line endings.Bernhard Schommer2016-03-211-1/+2
| |/ |/|
* | Preliminaries: extend the Coqlib and Maps libraries.Xavier Leroy2016-03-062-34/+189
|/
* Added printer for Configuration and finished Clflags.Bernhard Schommer2016-01-251-0/+9
* Started implementing a printer for Clflags.Bernhard Schommer2016-01-251-0/+33
* Open files in binary mode.Bernhard Schommer2015-11-301-2/+1
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-2018-1698/+1698
* Move more functionality in the new interface.Bernhard Schommer2015-09-161-9/+1
* Added symbol functions for printing of the location for global variables.Bernhard Schommer2015-08-211-0/+7
* Tighten and prove correct the underflow/overflow bounds for parsing of FP lit...Xavier Leroy2015-07-062-96/+220
* Give a name to the type of atoms.Xavier Leroy2015-04-231-2/+4
* remove not used hypotheses in TREEJacques-Henri Jourdan2015-03-251-9/+4
* Merge branch 'master' into no-shellBernhard Schommer2015-02-192-0/+139
|\
| * In -g -S mode, annotate the generated asm file with the C source code in comm...Xavier Leroy2015-01-072-0/+139
* | Use Unix.create_process instead of Sys.command to run external tools.Xavier Leroy2014-12-192-0/+150
|/
* build_from_parsed: simplified code + correctness proof.Xavier Leroy2014-11-151-15/+86
* Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-072-292/+106
* Add theorem "elements_remove".Xavier Leroy2014-09-241-167/+178
* More efficient implementations of map, fold, etc.xleroy2014-08-271-164/+109
* The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM.xleroy2014-07-281-73/+18
generated by cgit (git 2.34.1) at 2024-06-02 16:39:03 +0000