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
...
*
Remove support for x86-32 under macOS
Xavier Leroy
2020-07-29
2
-45
/
+3
*
Allow string_literals_list in _Static_assert.
Bernhard Schommer
2020-07-27
2
-24
/
+25
*
Add test for __builtin_sqrt and __builtin_fabsf
Xavier Leroy
2020-07-27
2
-0
/
+7
*
Add __builtin_sqrt as synonymous for __builtin_fsqrt
Xavier Leroy
2020-07-27
7
-5
/
+8
*
Refactor regression testing of built-in functions
Xavier Leroy
2020-07-27
13
-110
/
+447
*
Move declarations of __builtin_clz* and __builtin_ctz* to C2C.ml
Xavier Leroy
2020-07-27
5
-46
/
+12
*
AArch64 implementation of __builtin_ctz*
Xavier Leroy
2020-07-27
3
-1
/
+11
*
RISC-V implementation of __builtin_clz* and __builtin_ctz*
Xavier Leroy
2020-07-27
2
-0
/
+134
*
Add support for __builtin_fabsf
Xavier Leroy
2020-07-27
4
-0
/
+13
*
No need to process __builtin_fabs in $ARCH/Asmexpand.ml
Xavier Leroy
2020-07-27
5
-12
/
+0
*
More checks for __builtin_va_start (#250)
Bernhard Schommer
2020-07-21
1
-6
/
+10
*
cparser/handcrafted.messages: missing blank line
Xavier Leroy
2020-07-21
1
-0
/
+1
*
Updated handcrafted.messages.
Bernhard Schommer
2020-07-21
1
-0
/
+108
*
Support _Static_assert from C11
Xavier Leroy
2020-07-21
7
-1060
/
+1116
*
Support __builtin_constant_p as in GCC and Clang (#367)
Xavier Leroy
2020-07-21
1
-0
/
+10
*
Use the correct location for Slabaled in transform.
Bernhard Schommer
2020-07-21
1
-2
/
+2
*
Added error for redefined builtin.
Bernhard Schommer
2020-07-20
3
-0
/
+6
*
Added missing semicolon.
Bernhard Schommer
2020-07-15
1
-1
/
+1
*
Bytecode-only build, continued
Xavier Leroy
2020-07-15
1
-0
/
+9
*
Revised detection of menhirLib directory, continued (#365)
Xavier Leroy
2020-07-15
1
-4
/
+4
*
No trailing commas for --version-file option.
Bernhard Schommer
2020-07-09
1
-1
/
+1
*
Fix typo.
Bernhard Schommer
2020-07-08
1
-1
/
+1
*
Revert "Use the same version string."
Bernhard Schommer
2020-07-08
1
-3
/
+10
*
Use the same version string.
Bernhard Schommer
2020-07-08
1
-10
/
+3
*
Remove no longer needed option enforce-buildnr
Bernhard Schommer
2020-07-08
1
-10
/
+1
*
Introduce additional "branch" build information.
Bernhard Schommer
2020-07-08
7
-13
/
+20
*
Add option to print version information in file
Bernhard Schommer
2020-07-08
1
-1
/
+17
*
Bytecode-only build (#243)
Xavier Leroy
2020-07-07
2
-4
/
+29
*
Revised detection of menhirLib directory (#248)
Xavier Leroy
2020-07-07
1
-2
/
+6
*
Added asserts for constraints of PowerPC builtins
Bernhard Schommer
2020-07-01
1
-0
/
+6
*
Fix typo in name of builtin function.
Bernhard Schommer
2020-07-01
1
-1
/
+1
*
Added missing hint database name.
Bernhard Schommer
2020-06-30
1
-1
/
+1
*
Move shared code in new file.
Bernhard Schommer
2020-06-28
17
-96
/
+46
*
Remove the `can_reserve_register` function.
Bernhard Schommer
2020-06-28
10
-19
/
+1
*
Use library function.
Bernhard Schommer
2020-06-28
1
-4
/
+1
*
Use Hashtbl.find_opt.
Bernhard Schommer
2020-06-28
8
-9
/
+8
*
Eliminate known builtins whose result is ignored
Xavier Leroy
2020-06-25
2
-40
/
+54
*
Improve printing of builtin function invocations
Xavier Leroy
2020-06-25
1
-0
/
+3
*
Preliminary support for Coq 8.12
Xavier Leroy
2020-06-21
2
-4
/
+4
*
Transform non-recursive Fixpoint into Definition
Xavier Leroy
2020-06-21
3
-3
/
+3
*
SimplExpr: remove unused definition "sd_cast_set"
Xavier Leroy
2020-06-15
1
-2
/
+0
*
SimplExpr: better translation of casts in a "for effects" context
Xavier Leroy
2020-06-15
3
-136
/
+166
*
Compatibility with coq 8.11.2
Bernhard Schommer
2020-06-08
1
-1
/
+1
*
Improve portability of the test for annotations inclightgen
Xavier Leroy
2020-06-05
2
-0
/
+4
*
clightgen: fix the printing of annotations
Xavier Leroy
2020-06-05
2
-59
/
+14
*
clightgen: fix usage message
Xavier Leroy
2020-06-01
1
-2
/
+2
*
clightgen -short-idents : do not use $"xxx" notation ever
Xavier Leroy
2020-06-01
1
-1
/
+1
*
Add a canonical encoding of identifiers as numbers and use it in clightgen (#...
Xavier Leroy
2020-05-19
4
-20
/
+204
*
Move Commandline to the lib/ directory
Xavier Leroy
2020-05-05
2
-0
/
+0
*
Update the list of dual-licensed files
Xavier Leroy
2020-05-05
1
-2
/
+2
[prev]
[next]