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
*
Add `iter_literal*` functions with guaranteed iteration order
Xavier Leroy
2022-09-03
1
-0
/
+12
*
Rework of struct member offsets for debug info.
Bernhard Schommer
2022-09-03
6
-41
/
+92
*
Introduce `struct_layout` function
Bernhard Schommer
2022-09-03
2
-1
/
+28
*
Support mergeable sections for string literals and wide string literals
Xavier Leroy
2022-08-29
1
-6
/
+13
*
Support mergeable sections for fixed-size literals
Xavier Leroy
2022-08-29
11
-123
/
+145
*
configure: recognize riscv32 and riscv64 for RISC-V targets (#448)
Brad Smith
2022-08-29
1
-2
/
+3
*
Do not use `.rodata.cst8` for floating-point literals
Xavier Leroy
2022-08-15
2
-2
/
+2
*
Check early that extraction did not run into unimplemented axioms
Xavier Leroy
2022-07-07
1
-0
/
+5
*
Update comment about `deprecated-hint-rewrite-without-locality` warning
Xavier Leroy
2022-07-07
1
-4
/
+0
*
In test/regression: Use `static inline` instead of `inline`
Xavier Leroy
2022-07-05
2
-5
/
+5
*
Re-enable `deprecated-hint-rewrite-without-locality` warning
Xavier Leroy
2022-07-05
1
-2
/
+1
*
Add [#global] qualifier on Hint Rewrite (#439)
Pierre-Marie Pédrot
2022-07-05
2
-0
/
+12
*
More updates for release 3.11
Xavier Leroy
2022-06-27
1
-2
/
+2
*
Updates for release 3.11
Xavier Leroy
2022-06-25
2
-3
/
+6
*
Extend the boolean_equality tactic (#429)
Jerome Hugues
2022-06-25
1
-1
/
+15
*
Support Coq 8.15.2
Xavier Leroy
2022-06-25
2
-3
/
+3
*
Update comment re: compile_switch function
Xavier Leroy
2022-06-25
1
-1
/
+1
*
Expand "j_s symb" to "jump symb, x31" assembly pseudo-instruction
Xavier Leroy
2022-06-24
4
-5
/
+6
*
First Changelog update for next release 3.11
Xavier Leroy
2022-06-20
1
-0
/
+38
*
Harden the configure script against \r\n end of lines
Xavier Leroy
2022-06-20
1
-6
/
+6
*
AArch64: make register X29 callee-save
Xavier Leroy
2022-05-30
6
-34
/
+34
*
Improve control-flow analysis of "noreturn" function calls
Xavier Leroy
2022-05-19
1
-4
/
+18
*
Simplify handling of file suffixes.
Bernhard Schommer
2022-05-18
4
-30
/
+28
*
Fix computing of output filenames.
Bernhard Schommer
2022-05-18
1
-13
/
+15
*
Revised warning for non-prototyped function declarations
Xavier Leroy
2022-05-13
1
-17
/
+22
*
Some tests for _Generic
Xavier Leroy
2022-05-13
3
-1
/
+115
*
Support _Generic from ISO C 2011
Xavier Leroy
2022-05-13
7
-711
/
+1031
*
Fix the parsing of unprototyped function types in casts (#431)
Xavier Leroy
2022-05-09
1
-2
/
+2
*
Completely avoid line breaks in types when printing error messages
Xavier Leroy
2022-05-07
1
-6
/
+10
*
Enum is only compatible with IInt.
Xavier Leroy
2022-05-06
1
-4
/
+4
*
Merge pull request #368 from silene/flocq-3.4
Xavier Leroy
2022-04-29
38
-2934
/
+5149
|
\
|
*
Upgrade to Flocq 4.1.
Guillaume Melquiond
2022-04-26
11
-285
/
+737
|
*
Support Coq 8.15.1
Xavier Leroy
2022-04-25
1
-2
/
+2
|
*
Make Coq 8.12.0 the minimal version.
Guillaume Melquiond
2022-04-25
1
-2
/
+2
|
*
Ignore .coq-native directories.
Guillaume Melquiond
2022-04-25
1
-0
/
+1
|
*
Upgrade to Flocq 4.0.
Guillaume Melquiond
2022-04-25
36
-2875
/
+4637
|
/
*
Fix a typo in a comment in Clight.v (#427)
Hanzhi Liu
2022-04-25
1
-1
/
+1
*
Introduce float_conversion_default_nan parameter for float-float conversions
Bernhard Schommer
2022-04-25
7
-9
/
+31
*
Check for arguments of struct/union type passed to a vararg function
Xavier Leroy
2022-02-11
1
-13
/
+16
*
Add op for float max and min for x86.
Bernhard Schommer
2022-02-07
10
-23
/
+66
*
Return second arg for float min/max on x86.
Bernhard Schommer
2022-02-07
1
-4
/
+4
*
Support Coq 8.15.0
Xavier Leroy
2022-01-31
1
-2
/
+2
*
Adapt w.r.t. coq/coq#15442 (#425)
Pierre-Marie Pédrot
2022-01-10
3
-6
/
+6
*
Fix pattern for github-linguist.
Bernhard Schommer
2021-12-14
1
-2
/
+2
*
Enforce evaluation order in IRC.add_interf and IRC.add_pref
Xavier Leroy
2021-12-07
1
-2
/
+2
*
Support Coq 8.14.1
Xavier Leroy
2021-11-26
1
-2
/
+2
*
Second update for release 3.10
v3.10
Xavier Leroy
2021-11-19
1
-4
/
+6
*
mention AArch64 in man-page
Michael Schmidt
2021-11-17
1
-1
/
+1
*
Remove documentation of bitfield language support option.
Michael Schmidt
2021-11-17
1
-5
/
+0
*
First update for release 3.10
Xavier Leroy
2021-11-16
3
-2
/
+57
[next]