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
*
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
*
Changed cc_varargs to an option type
Bernhard Schommer
2020-12-25
12
-27
/
+36
*
configure: use `$make` instead of `make`
Xavier Leroy
2020-12-25
1
-1
/
+1
*
configure script revised and simplified
Xavier Leroy
2020-12-24
1
-83
/
+43
*
configure: support Coq 8.12.2
Xavier Leroy
2020-12-24
1
-2
/
+2
*
Configure the correct archiver to build runtime/libcompcert.a
Xavier Leroy
2020-12-24
2
-2
/
+8
*
x86 32 bits: ABI non-conformance for functions returning structs/unions
Xavier Leroy
2020-12-11
1
-1
/
+1
*
Error when using -main without -interp
Xavier Leroy
2020-12-06
1
-0
/
+2
*
PowerPC modeling of registers destroyed by pseudo-instructions
Xavier Leroy
2020-12-06
2
-4
/
+6
*
ARM modeling of registers destroyed by pseudo-instructions
Xavier Leroy
2020-12-06
2
-4
/
+6
*
AArch64 modeling of registers destroyed by pseudo-instructions
Xavier Leroy
2020-12-06
2
-8
/
+11
*
Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructions
Xavier Leroy
2020-12-06
12
-99
/
+23
*
Updates for release 3.8
v3.8
Xavier Leroy
2020-11-16
3
-5
/
+10
*
Do not use -warn-error when building from a release tarball
Xavier Leroy
2020-11-14
1
-2
/
+9
*
Support Coq 8.12.1
Xavier Leroy
2020-11-14
2
-3
/
+3
*
Update README
Xavier Leroy
2020-11-09
1
-4
/
+4
*
Update Changes
Xavier Leroy
2020-11-08
1
-0
/
+48
*
Added semantics for the PowerPC sel and mulh built-ins
Bernhard Schommer
2020-11-07
1
-4
/
+44
*
Added missing printer for PowerPC 64 bit comparison.
Bernhard Schommer
2020-11-06
1
-0
/
+8
*
Added implementation for fmin/fmax for aarch64.
Bernhard Schommer
2020-11-06
3
-0
/
+12
*
Better "make clean"
Xavier Leroy
2020-11-01
1
-1
/
+1
*
Add -main option to specify entrypoint function in interpreter mode (#374)
Xavier Leroy
2020-10-30
4
-20
/
+42
*
Add `string_of_ident` conversion
Xavier Leroy
2020-10-12
1
-0
/
+110
*
Remove -version-file option
Xavier Leroy
2020-10-12
1
-19
/
+2
*
Support Cygwin 64 bits
Xavier Leroy
2020-10-05
17
-118
/
+415
*
Test clightgen with -short-idents and -normalize options
Xavier Leroy
2020-09-22
1
-0
/
+6
*
Use exact arithmetic for printing positive numbers
Xavier Leroy
2020-09-22
1
-52
/
+56
*
Fix computation of next temporary in -canonical-idents mode
Xavier Leroy
2020-09-22
1
-1
/
+12
*
Support the use of already-installed MenhirLib and Flocq libraries
Xavier Leroy
2020-09-21
11
-67
/
+82
*
No need for -R options, _CoqProject contains them already
Xavier Leroy
2020-09-21
1
-4
/
+2
*
Check ptr arithmetic for ++ and --
Bernhard Schommer
2020-09-20
1
-10
/
+16
*
Simplify two scripts in Zbits (#369)
Maxime Dénès
2020-09-18
1
-2
/
+2
*
Add new static-assert token for deLexer utility; bug 29273
Michael Schmidt
2020-08-04
1
-0
/
+1
*
Add comments we missed to sync to GitHub
Christoph Cullmann
2020-07-30
1
-0
/
+2
[next]