index
:
compcert
FPcomp
aarch64
conditional-move
dev/michalis
floatofintu
inl-cse-const
master
no-pervasives
CompCert fork with minor modifications for Vericert.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
lib
Commit message (
Expand
)
Author
Age
Files
Lines
*
Resynchronize the LICENSE file and the license headers in individual files (#45)
Xavier Leroy
2018-01-05
6
-251
/
+15
*
Test for inline. Bug 22642
Bernhard Schommer
2017-12-08
1
-1
/
+1
*
Added simple div_one Theorem variants.
Bernhard Schommer
2017-12-01
1
-0
/
+6
*
New json printing interface.
Bernhard Schommer
2017-11-14
3
-1
/
+190
*
Merge pull request #191 from sigurdschneider/master
Xavier Leroy
2017-10-20
3
-2
/
+3
|
\
|
*
Ensure FunInd or Recdef is imported if functional induction is used
Sigurd Schneider
2017-07-20
3
-2
/
+3
*
|
Remove coq warnings (#28)
Bernhard Schommer
2017-09-22
11
-182
/
+182
*
|
Some lemmas.
Bernhard Schommer
2017-09-21
1
-0
/
+14
|
/
*
Formatted json printing.
Bernhard Schommer
2017-06-28
1
-22
/
+32
*
Hybrid 64bit/32bit PowerPC port
Bernhard Schommer
2017-05-03
5
-70
/
+230
*
RISC-V port and assorted changes
Xavier Leroy
2017-04-28
2
-3
/
+25
*
Adapt proofs to future handling of literal constants in Coq.
Guillaume Melquiond
2017-03-08
1
-5
/
+2
*
Replace "Implicit Arguments" with "Arguments"
Xavier Leroy
2017-02-13
2
-6
/
+4
*
Use "Local" as prefix
Xavier Leroy
2017-02-13
1
-1
/
+1
*
Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.v
Xavier Leroy
2016-12-26
1
-0
/
+167
*
C2C: revise typing and translation of __builtin_memcpy_aligned
Xavier Leroy
2016-11-17
1
-0
/
+6
*
Finish the proofs of SelectLong for IA32
Xavier Leroy
2016-10-02
1
-1
/
+108
*
Improve code generation for 64-bit signed integer division
Xavier Leroy
2016-10-02
1
-0
/
+37
*
Support for 64-bit architectures: generic support
Xavier Leroy
2016-10-01
1
-3
/
+454
*
IA32: model integer division and modulus closer to the machine
Xavier Leroy
2016-09-18
1
-0
/
+92
*
Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpy
Xavier Leroy
2016-09-17
1
-0
/
+28
*
Decidableplus: remove stuff that was cut-and-paste from Coq 8.5 library
Xavier Leroy
2016-09-17
1
-48
/
+1
*
Removed some implict arguments.
Bernhard Schommer
2016-09-05
1
-5
/
+3
*
Moved quoting functions in Responsefile
Bernhard Schommer
2016-08-16
2
-2
/
+36
*
Added simplified reader and printer for gnu @files
Bernhard Schommer
2016-07-20
3
-134
/
+98
*
Added heuristic for passing arg via responsefiles.
Bernhard Schommer
2016-07-12
2
-20
/
+0
*
Really added the function. Bug 18308
Bernhard Schommer
2016-07-11
2
-3
/
+19
*
Added function to write responsefiles.
Bernhard Schommer
2016-07-11
1
-0
/
+24
*
Merge branch 'master' into add-file
Bernhard Schommer
2016-07-11
10
-173
/
+156
|
\
|
*
Port to Coq 8.5pl2
Xavier Leroy
2016-07-08
10
-173
/
+156
*
|
Added responsefile support for commandline.
Bernhard Schommer
2016-07-08
1
-0
/
+133
|
/
*
Remove code that will is deprecated in ocaml 4.03
Bernhard Schommer
2016-06-21
1
-0
/
+10
*
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
[next]