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
Commit message (
Expand
)
Author
Age
Files
Lines
*
Fix spurious error on initialization of struct with flexible array member
Xavier Leroy
2021-05-02
1
-0
/
+3
*
Update Changelog
Xavier Leroy
2021-04-29
1
-0
/
+53
*
Emit no entry for variables without init in json.
Bernhard Schommer
2021-04-29
1
-1
/
+7
*
MacOS: add a #define __DARWIN_OS_INLINE
Xavier Leroy
2021-04-27
1
-2
/
+2
*
Support Coq 8.13.2
Xavier Leroy
2021-04-27
1
-2
/
+2
*
More fixes for ld/std issue.
Bernhard Schommer
2021-04-24
1
-11
/
+40
*
Tentative first fix for offsets of ld/std.
Bernhard Schommer
2021-04-24
5
-152
/
+259
*
Update the output of clightgen to pick the `$` notation from its new place
Xavier Leroy
2021-04-23
1
-1
/
+3
*
Remove `-version-file` option from option summary
Xavier Leroy
2021-04-23
1
-1
/
+0
*
Move `$` notation in submodule `ClightNotations` and scope `clight_scope`
Xavier Leroy
2021-04-23
1
-11
/
+23
*
Use List.repeat from Coq's standard library instead of list_repeat
Xavier Leroy
2021-04-19
4
-36
/
+16
*
Bump minimal Coq version to 8.9.0
Xavier Leroy
2021-04-19
1
-2
/
+2
*
Elab bitfields: check size of type <=32bit rather than checking rank (#387)
Amos Robinson
2021-04-19
4
-2
/
+25
*
Refactor cparser/Parse.ml
Xavier Leroy
2021-04-19
1
-31
/
+29
*
Ensure compatibility with future versions of MenhirLib
Xavier Leroy
2021-04-19
1
-6
/
+7
*
Do not depend on projection parameter names (#388)
Xia Li-yao
2021-03-25
1
-1
/
+1
*
Coq 8.13.1 is supported
Xavier Leroy
2021-03-09
1
-2
/
+2
*
Fix regression on PowerPC / Diab
Xavier Leroy
2021-02-23
2
-4
/
+11
*
Section handling: finer control of variable initialization
Xavier Leroy
2021-02-23
9
-42
/
+90
*
Introduce and use PrintAsmaux.variable_section
Xavier Leroy
2021-02-23
6
-35
/
+34
*
Silence some new warnings of Coq 8.13
Xavier Leroy
2021-01-21
1
-1
/
+17
*
Qualify `Hint` as `Global Hint` where appropriate
Xavier Leroy
2021-01-21
30
-133
/
+136
*
Define `fold_ind_aux` and `fold_ind` transparently
Xavier Leroy
2021-01-21
1
-2
/
+2
*
"macosx" is now called "macos"
Xavier Leroy
2021-01-18
16
-25
/
+25
*
macOS: turn #warning off
Xavier Leroy
2021-01-18
1
-2
/
+2
*
Remove regression/interop1 test
Xavier Leroy
2021-01-18
4
-417
/
+1
*
Testing calling conventions and interoperability with another C compiler
Xavier Leroy
2021-01-18
5
-1
/
+583
*
Support re-normalization of function parameters at function entry
Xavier Leroy
2021-01-16
7
-27
/
+58
*
Change warning for pragmas inside functions
Xavier Leroy
2021-01-16
1
-1
/
+1
*
PowerPC: wrong computation of the position of the first vararg argument
Xavier Leroy
2021-01-15
1
-2
/
+3
*
Coq 8.13.0 is supported
Xavier Leroy
2021-01-14
1
-3
/
+3
*
RISC-V: fix FP calling conventions
Xavier Leroy
2021-01-14
6
-122
/
+176
*
Replace `omega` tactic with `lia`, continued
Xavier Leroy
2021-01-13
1
-1
/
+1
*
Improve branch tunneling
Xavier Leroy
2021-01-13
2
-60
/
+328
*
Revised correctness proof for record_goto
Xavier Leroy
2021-01-13
1
-68
/
+29
*
Add new fold_ind induction principle for folds
Xavier Leroy
2021-01-13
1
-63
/
+82
*
Add lemma list_norepet_rev
Xavier Leroy
2021-01-13
1
-0
/
+8
*
RISC-V: wrong fixup code generated for vararg calls with fixed FP args
Xavier Leroy
2021-01-10
3
-12
/
+35
*
Ignore and warn about pragmas inside functions
Xavier Leroy
2021-01-07
1
-1
/
+4
*
Replace `omega` tactic with `lia`
Xavier Leroy
2020-12-29
110
-2695
/
+2694
*
Remove useless parameters in theorems int_round_odd_bits and int_round_odd_le
Xavier Leroy
2020-12-29
2
-13
/
+13
*
Update Flocq to 3.4.0 (#383)
Guillaume Melquiond
2020-12-28
30
-638
/
+1841
*
configure: simplify the final printing of the configuration
Xavier Leroy
2020-12-28
1
-9
/
+8
*
configure: add -mandir option (#382)
Daniel Dickman
2020-12-28
1
-1
/
+7
*
AArch64 / macOS: use __DATA,__CONST section instead of .const (temporary fix)
Xavier Leroy
2020-12-26
1
-1
/
+1
*
AArch64: macOS port
Xavier Leroy
2020-12-26
18
-220
/
+570
*
C parser: handle other built-in types than __builtin_va_list
Xavier Leroy
2020-12-26
1
-1
/
+2
*
AArch64: clarify the printing of extending-register arithmetic operations
Xavier Leroy
2020-12-26
1
-13
/
+13
*
AArch64: wrong function alignment
Xavier Leroy
2020-12-26
1
-1
/
+1
*
RISC-V: revised calling conventions for variadic functions
Xavier Leroy
2020-12-25
2
-63
/
+105
[next]