index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
common
/
AST.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
[BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...
Cyril SIX
2021-06-01
1
-4
/
+5
*
Merge branch 'master' into merge_master_8.13.1
Sylvain Boulmé
2021-03-23
1
-8
/
+8
|
\
|
*
Replace `omega` tactic with `lia`
Xavier Leroy
2020-12-29
1
-3
/
+3
|
*
Changed cc_varargs to an option type
Bernhard Schommer
2020-12-25
1
-5
/
+5
*
|
Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8
David Monniaux
2020-11-18
1
-1
/
+1
|
\
|
|
*
Transform non-recursive Fixpoint into Definition
Xavier Leroy
2020-06-21
1
-1
/
+1
*
|
print hashes
David Monniaux
2020-04-08
1
-2
/
+3
*
|
begin installing profiling
David Monniaux
2020-04-08
1
-4
/
+5
*
|
added EF_profiling
David Monniaux
2020-04-08
1
-1
/
+9
*
|
Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...
David Monniaux
2020-03-03
1
-1
/
+28
|
\
\
|
|
/
|
/
|
|
*
Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load
David Monniaux
2019-12-02
1
-1
/
+18
|
|
\
|
|
*
Ibuiltin proof
Cyril SIX
2019-10-04
1
-1
/
+18
|
*
|
more proofs going through
David Monniaux
2019-09-05
1
-0
/
+1
|
*
|
moved trapping_mode to a more appropriate place
David Monniaux
2019-09-03
1
-0
/
+9
|
|
/
*
/
Refine the type of function results in AST.signature
Xavier Leroy
2020-02-21
1
-20
/
+59
|
/
*
Fix misspellings in messages, man pages, and comments
Xavier Leroy
2019-05-31
1
-2
/
+2
*
New support for inserting ais-annotations.
Bernhard Schommer
2017-10-19
1
-7
/
+7
*
Remove coq warnings (#28)
Bernhard Schommer
2017-09-22
1
-1
/
+1
*
Extend builtin arguments with a pointer addition operator
Xavier Leroy
2017-07-06
1
-14
/
+7
*
Hybrid 64bit/32bit PowerPC port
Bernhard Schommer
2017-05-03
1
-7
/
+7
*
Replace "Implicit Arguments" with "Arguments"
Xavier Leroy
2017-02-13
1
-3
/
+3
*
Support for 64-bit architectures: generic support
Xavier Leroy
2016-10-01
1
-12
/
+26
*
Unwanted partial constant propagation in 64-bit integer arguments to builtins
Xavier Leroy
2016-07-08
1
-1
/
+1
*
Introduce register pairs to describe calling conventions more precisely
Xavier Leroy
2016-05-17
1
-1
/
+56
*
AST: extend and adapt to the new linking framework.
Xavier Leroy
2016-03-06
1
-460
/
+116
*
Updated PR by removing whitespaces. Bug 17450.
Bernhard Schommer
2015-10-20
1
-37
/
+37
*
Use Coq strings instead of idents to name external and builtin functions.
Xavier Leroy
2015-10-11
1
-12
/
+8
*
Added versions of the tranform_* functions in AST to work with functions
Bernhard Schommer
2015-10-08
1
-1
/
+216
*
Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.
Xavier Leroy
2015-08-22
1
-10
/
+10
*
Refactoring of builtins and annotations in the back-end.
Xavier Leroy
2015-08-21
1
-58
/
+85
*
In AST.calling_conventions, record whether the original C function was "old-s...
Xavier Leroy
2015-05-22
1
-3
/
+4
*
Extended inline asm: revised treatment of clobbered registers.
Xavier Leroy
2015-05-09
1
-2
/
+2
*
Support for GCC-style extended asm, continued:
Xavier Leroy
2015-04-21
1
-3
/
+4
*
Experiment: support a subset of GCC's extended asm statements.
Xavier Leroy
2015-04-17
1
-3
/
+3
*
Extend annotations so that they can keep track of global variables and local ...
Xavier Leroy
2015-03-27
1
-16
/
+57
*
Add Genv.public_symbol operation.
Xavier Leroy
2014-11-24
1
-0
/
+9
*
Record public global definitions via field "prog_public" in AST.program.
Xavier Leroy
2014-11-24
1
-3
/
+25
*
Merge of "newspilling" branch:
xleroy
2014-07-23
1
-33
/
+35
*
Type-checking of builtin volatile write Mfloat32 was too strict, causing type...
xleroy
2014-03-24
1
-2
/
+2
*
- Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.
xleroy
2014-01-12
1
-5
/
+2
*
Simpler, more robust emulation of calls to variadic functions:
xleroy
2013-12-28
1
-16
/
+34
*
Merge of the float32 branch:
xleroy
2013-05-19
1
-4
/
+69
*
Refactoring: move definition of chunk_of_type to AST.v.
xleroy
2013-05-06
1
-0
/
+10
*
Coq-defined equality functions for Allocation.
xleroy
2013-05-01
1
-3
/
+20
*
Big merge of the newregalloc-int64 branch. Lots of changes in two directions:
xleroy
2013-04-20
1
-15
/
+24
*
Glasnost: making transparent a number of definitions that were opaque
xleroy
2013-03-10
1
-2
/
+4
*
Constant propagation within __builtin_annot.
xleroy
2013-02-24
1
-3
/
+15
*
Ported to Coq 8.4pl1. Merge of branches/coq-8.4.
xleroy
2013-01-29
1
-6
/
+6
*
Support for inline assembly (asm statements).
xleroy
2012-12-18
1
-1
/
+9
*
Globalenvs: allocate one-byte block with permissions Nonempty for each
xleroy
2012-11-12
1
-253
/
+169
[next]