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
...
*
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
*
Dual-license aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v}
Xavier Leroy
2020-05-05
3
-0
/
+9
*
Import ListNotations explicitly
Xavier Leroy
2020-05-04
1
-0
/
+1
*
Revert "Do not use the list notation `[]`"
Xavier Leroy
2020-05-04
1
-8
/
+8
*
Do not use the list notation `[]`
Xavier Leroy
2020-05-04
1
-8
/
+8
*
Do not use "Declare Scope", introduced in Coq 8.10 only
Xavier Leroy
2020-05-04
1
-1
/
+0
*
Coq-MenhirLib: explicit import ListNotations (#354)
Jacques-Henri Jourdan
2020-05-04
7
-4
/
+12
*
Install "compcert.config" file along the Coq development
Xavier Leroy
2020-04-29
2
-1
/
+19
*
Updated .gitignore
Bernhard Schommer
2020-04-27
1
-0
/
+1
*
Simplify the generation of driver/Version.ml
Bernhard Schommer
2020-04-27
1
-3
/
+8
*
Move reserved_registers to CPragmas.
Bernhard Schommer
2020-04-20
4
-8
/
+8
*
Support for coq 8.11.1.
Bernhard Schommer
2020-04-20
1
-2
/
+2
*
Check for errors after each pass.
Bernhard Schommer
2020-04-20
1
-1
/
+8
*
Added warning for packed composite with bitfields.
Bernhard Schommer
2020-04-20
1
-0
/
+2
*
Add location to transform functions.
Bernhard Schommer
2020-04-20
4
-28
/
+28
[prev]
[next]