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