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
*
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
*
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
[next]