C

CompCert

Settings | Report Duplicate

1

I Use This!

Moderate Activity

Commits : Listings

Analyzed about 21 hours ago. based on code collected about 21 hours ago.

Commit Message	Contributor	Files Modified	Lines Added	Lines Removed	Code Location	Date
Jul 22, 2024 — Jul 22, 2025 Showing page 88 of 108 Search / Filter on:
Better locations for error messages relative to type specifiers.	xleroy	More...				over 12 years ago
Watch out for behaviors exponential in the nesting of struct/union types.	xleroy	More...				over 12 years ago
RTLtyping: now performed entirely in Coq, no need for an external Caml oracle + a validator.	xleroy	More...				over 12 years ago
Update clightgen to changes in Camlcoq and in AST.	xleroy	More...				over 12 years ago
Diab asm syntax issue	xleroy	More...				over 12 years ago
For Pfreeframe, generate an "addi" over GPR1 when possible, to work around a limitation in the a3 analyzers.	xleroy	More...				over 12 years ago
Remove the C primitives for unsigned long long arithmetic, replaced by pure OCaml code.	xleroy	More...				over 12 years ago
More aggressive CSE across Ibuiltin.	xleroy	More...				over 12 years ago
Assorted changes to reduce stack and heap requirements when compiling very big functions.	xleroy	More...				over 12 years ago
Machsem: no longer useful.	xleroy	More...				over 12 years ago
Bind some local defs with Let, makes extracted code cleaner	xleroy	More...				over 12 years ago
Maps: revised TREE interface; added mucho derived properties and operations in Tree_Properties. Lattice: adapted accordingly.	xleroy	More...				over 12 years ago
Suppress int64_unsigned_to_float, now unused.	xleroy	More...				over 12 years ago
More updates for 1.13	xleroy	More...				over 12 years ago
Fixed parsing of hex float literals 0xNNNpMMM.	xleroy	More...				over 12 years ago
Updated for version 1.13	xleroy	More...				over 12 years ago
Updating doc for 1.13	xleroy	More...				over 12 years ago
Useless Import	xleroy	More...				over 12 years ago
Glasnost: making transparent a number of definitions that were opaque for no good reason.	xleroy	More...				over 12 years ago
Assorted cleanups, esp. to avoid generating _rec and _rect recursors in submodules. (Extraction does not remove them, then.) common/Switch: replaced use of FMaps by our own Maps.	xleroy	More...				over 12 years ago
Improving the performance of exhaustive exploration (mode -all): - Re-share states even at different times - Faster comparison between states, giving priority to the mem nextblock	xleroy	More...				over 12 years ago
Finished backtracking (cf previous commit) for ARM and PowerPC. ARM: slightly shorter code generated for indirect memory accesses.	xleroy	More...				over 12 years ago
Partial backtracking on previous commit: the "hole in Mach stack frame" trick prevents a future mapping of the Mach/Asm call stack as a single block. IA32 is fixed, PowerPC and ARM remains to be done.	xleroy	More...				over 12 years ago
Updates to follow recent changes in PrintAsm.ml	xleroy	More...				over 12 years ago
Some builtins were renamed, updating	xleroy	More...				over 12 years ago
Bug in Pbtbl	xleroy	More...				over 12 years ago
No longer a dependency on Machtyping	xleroy	More...				over 12 years ago
Fix 'interp' entry	xleroy	More...				over 12 years ago
Testing dense switches	xleroy	More...				over 12 years ago
Revised Stacking and Asmgen passes and Mach semantics: - no more prediction of return addresses (Asmgenretaddr is gone) - instead, punch a hole for the retaddr in Mach stack frame and fill this hole with the return address in the Asmgen proof.	xleroy	More...				over 12 years ago

←
1
2
…
84
85
86
87
88
89
90
91
92
…
107
108
→