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
*
Resurrect a warning for bit fields of enum types
Xavier Leroy
2021-11-12
1
-15
/
+33
*
PPC64: revised generation of rldic* instructions
Xavier Leroy
2021-10-28
4
-20
/
+31
*
Explicitly remove __SIZEOF_INT128__ macro definition. (#419)
roconnor-blockstream
2021-10-16
1
-4
/
+4
*
Merge pull request #415 from AbsInt/coq-8.14-compat
Xavier Leroy
2021-10-16
18
-58
/
+68
|
\
|
*
Add Coq 8.14.0 to the supported versions of Coq
Xavier Leroy
2021-10-03
1
-3
/
+3
|
*
Selectively turn some Coq 8.14 warnings off
Xavier Leroy
2021-10-03
1
-1
/
+11
|
*
Qualify `Instance` and `Program Instance` as `Global`
Xavier Leroy
2021-10-03
15
-53
/
+53
|
*
Vendored Flocq library: address Coq 8.14 warning
Xavier Leroy
2021-10-03
1
-1
/
+1
|
/
*
Synchronize vendored MenhirLib with upstream (#416)
Jacques-Henri Jourdan
2021-10-03
7
-36
/
+47
*
Adapt to coq/coq#13837 ("apply with" does not rename arguments) (#417)
Gaƫtan Gilbert
2021-10-03
2
-4
/
+4
*
Typo in expand_builtin_memcpy_small
Xavier Leroy
2021-10-01
1
-1
/
+1
*
Ignore unnamed bit fields for initialization of unions
Bernhard Schommer
2021-09-28
2
-7
/
+16
*
Ignore unnamed plain members of structs and unions
Xavier Leroy
2021-09-28
1
-10
/
+15
*
Merge pull request #413 from AbsInt/new-export
Xavier Leroy
2021-09-27
27
-694
/
+1098
|
\
|
*
Update export/README.md
Xavier Leroy
2021-09-22
1
-18
/
+18
|
*
Add support to clightgen for generating Csyntax AST as .v files
Xavier Leroy
2021-09-22
21
-271
/
+625
|
*
Refactor clightgen
Xavier Leroy
2021-09-22
13
-594
/
+644
*
|
Vendored MenhirLib: replace Require Omega with Require ZArith
Xavier Leroy
2021-09-25
1
-1
/
+1
*
|
Update the vendored Flocq library to version 3.4.2
Xavier Leroy
2021-09-25
5
-38
/
+24
*
|
Fix wrong expansion of __builtin_memcpy_aligned
Xavier Leroy
2021-09-23
4
-8
/
+8
*
|
For __builtin_memcpy_aligned, watch out for alignment of stack offsets
Xavier Leroy
2021-09-23
1
-0
/
+1
|
/
*
Fix the type and the semantics of BI_bsel
Xavier Leroy
2021-09-22
1
-4
/
+17
*
For numerical builtins, support return types that are small integer types
Xavier Leroy
2021-09-22
1
-25
/
+47
*
Avoid `Global Set Asymmetric Patterns` (#408)
Xavier Leroy
2021-09-15
8
-5
/
+13
*
clightgen: handle empty names given to padding bit fields
Xavier Leroy
2021-09-15
2
-16
/
+28
*
Handle the new warnings of OCaml 4.13
Xavier Leroy
2021-09-13
2
-4
/
+4
*
Share code for memory access for PowerPC
Bernhard Schommer
2021-09-06
4
-166
/
+159
*
Protect against overflows in `leaq` (all forms)
Bernhard Schommer
2021-08-27
1
-22
/
+27
*
Protect against overflows in `leaq N(src), dst` (#407)
Xavier Leroy
2021-08-27
1
-12
/
+17
*
Merge branch 'bitfields' (#400)
Xavier Leroy
2021-08-22
45
-2305
/
+4004
|
\
|
*
Native support for bit fields (#400)
Xavier Leroy
2021-08-22
42
-2299
/
+3866
|
*
Add Ctypes.link_match_program_gen
Xavier Leroy
2021-08-22
1
-0
/
+52
|
*
Int.sign_ext_shr_shl: weaker hypothesis
Xavier Leroy
2021-08-22
3
-6
/
+6
|
*
Add `floor` and some properties
Xavier Leroy
2021-07-26
1
-0
/
+37
|
*
More lemmas about `align`
Xavier Leroy
2021-07-26
1
-0
/
+17
|
*
More lemmas about list append
Xavier Leroy
2021-07-26
1
-0
/
+26
*
|
Revise the declaration of __compcert_* helper functions
Xavier Leroy
2021-06-30
1
-82
/
+79
*
|
x86 assembly: fix the comment delimiter for macos and make it per-OS
Xavier Leroy
2021-06-10
1
-3
/
+11
*
|
Support `# 0 ...` preprocessed line directive
Xavier Leroy
2021-06-01
1
-1
/
+1
|
/
*
Register X1 is destroyed by some built-in functions
Xavier Leroy
2021-05-13
2
-3
/
+5
*
Update for release 3.9
v3.9
Xavier Leroy
2021-05-10
1
-1
/
+1
*
Update Changelog for release 3.9
Xavier Leroy
2021-05-09
1
-0
/
+3
*
Update for release 3.9
Xavier Leroy
2021-05-09
1
-4
/
+5
*
Update Changelog
Xavier Leroy
2021-05-08
1
-1
/
+11
*
Use the LGPL instead of the GPL for dual-licensed files
Xavier Leroy
2021-05-08
149
-860
/
+1171
*
Fix evaluation order in emulation of bitfield assignment
Xavier Leroy
2021-05-02
1
-2
/
+2
*
Support __builtin_expect
Xavier Leroy
2021-05-02
1
-0
/
+5
*
Support __builtin_unreachable
Xavier Leroy
2021-05-02
8
-2
/
+32
*
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
[next]