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
Commit message (
Expand
)
Author
Age
Files
Lines
*
Adding debug info
nicolas.nardino
2021-06-06
1
-42
/
+53
*
Fixing scope error, and non-exhaustive pattern matching
nicolas.nardino
2021-06-06
1
-5
/
+6
*
function written, now needs testing
nicolas.nardino
2021-06-05
1
-10
/
+40
*
computing live regs at sb entry from its live output regs
nicolas.nardino
2021-06-04
2
-6
/
+24
*
Passing info of live regs to scheduler: beginning
nicolas.nardino
2021-06-04
5
-2
/
+17
*
Remove install path bricolage for kvx
v3.9_kvx
Cyril SIX
2021-06-01
2
-4
/
+5
*
Merge remote-tracking branch 'verimag/manuscript' into kvx-work
Cyril SIX
2021-06-01
1
-13
/
+11
|
\
|
*
Do not rotate if the CB was already at the end.
Cyril SIX
2021-04-28
1
-1
/
+5
|
*
Heuristic counter update
Cyril SIX
2021-04-28
1
-12
/
+6
*
|
Update INSTALL.md
Cyril SIX
2021-06-01
1
-0
/
+6
*
|
Fixing build for KVX (missing ccomp_kvx_fixes.h for runtime)
Cyril SIX
2021-06-01
1
-0
/
+1
*
|
Add target ELF
Cyril SIX
2021-06-01
4
-2
/
+7
*
|
Merge remote-tracking branch 'absint/master' into kvx-work
Cyril SIX
2021-06-01
3
-4
/
+6
|
\
\
|
*
|
Support `# 0 ...` preprocessed line directive
Xavier Leroy
2021-06-01
1
-1
/
+1
|
*
|
Register X1 is destroyed by some built-in functions
Xavier Leroy
2021-05-13
2
-3
/
+5
|
*
|
Update for release 3.9
Xavier Leroy
2021-05-10
1
-1
/
+1
|
*
|
Update Changelog for release 3.9
Xavier Leroy
2021-05-09
1
-0
/
+3
|
*
|
Update for release 3.9
Xavier Leroy
2021-05-09
1
-4
/
+5
|
*
|
Update Changelog
Xavier Leroy
2021-05-08
1
-1
/
+11
|
*
|
Use the LGPL instead of the GPL for dual-licensed files
Xavier Leroy
2021-05-08
149
-860
/
+1171
|
*
|
Fix evaluation order in emulation of bitfield assignment
Xavier Leroy
2021-05-02
1
-2
/
+2
|
*
|
Support __builtin_expect
Xavier Leroy
2021-05-02
1
-0
/
+5
|
*
|
Support __builtin_unreachable
Xavier Leroy
2021-05-02
8
-2
/
+32
|
*
|
Fix spurious error on initialization of struct with flexible array member
Xavier Leroy
2021-05-02
1
-0
/
+3
|
*
|
Update Changelog
Xavier Leroy
2021-04-29
1
-0
/
+53
|
*
|
Emit no entry for variables without init in json.
Bernhard Schommer
2021-04-29
1
-1
/
+7
|
*
|
MacOS: add a #define __DARWIN_OS_INLINE
Xavier Leroy
2021-04-27
1
-2
/
+2
|
*
|
Support Coq 8.13.2
Xavier Leroy
2021-04-27
1
-2
/
+2
|
*
|
More fixes for ld/std issue.
Bernhard Schommer
2021-04-24
1
-11
/
+40
|
*
|
Tentative first fix for offsets of ld/std.
Bernhard Schommer
2021-04-24
5
-152
/
+259
|
*
|
Update the output of clightgen to pick the `$` notation from its new place
Xavier Leroy
2021-04-23
1
-1
/
+3
|
*
|
Remove `-version-file` option from option summary
Xavier Leroy
2021-04-23
1
-1
/
+0
|
*
|
Move `$` notation in submodule `ClightNotations` and scope `clight_scope`
Xavier Leroy
2021-04-23
1
-11
/
+23
|
*
|
Use List.repeat from Coq's standard library instead of list_repeat
Xavier Leroy
2021-04-19
4
-36
/
+16
|
*
|
Bump minimal Coq version to 8.9.0
Xavier Leroy
2021-04-19
1
-2
/
+2
|
*
|
Elab bitfields: check size of type <=32bit rather than checking rank (#387)
Amos Robinson
2021-04-19
4
-2
/
+25
|
*
|
Refactor cparser/Parse.ml
Xavier Leroy
2021-04-19
1
-31
/
+29
|
*
|
Ensure compatibility with future versions of MenhirLib
Xavier Leroy
2021-04-19
1
-6
/
+7
|
*
|
Do not depend on projection parameter names (#388)
Xia Li-yao
2021-03-25
1
-1
/
+1
*
|
|
Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1
Cyril SIX
2021-06-01
77
-1940
/
+4260
|
\
\
\
|
*
|
|
removing some Expansion when loading float/single constants
Léo Gourdin
2021-06-01
1
-16
/
+22
|
*
|
|
Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...
Léo Gourdin
2021-05-31
1
-1
/
+0
|
|
\
\
\
|
|
*
|
|
just remove a debug print
Léo Gourdin
2021-05-29
1
-1
/
+0
|
*
|
|
|
bugfix A64 peephole (cf Scade/Fighter example)
Léo Gourdin
2021-05-31
1
-6
/
+5
|
|
/
/
/
|
*
|
|
Adding both RV expansion methods in kvx-work
Léo Gourdin
2021-05-19
8
-48
/
+1410
|
*
|
|
Merge branch 'riscv-work-fpinit-stillexp' into kvx-work
Léo Gourdin
2021-05-19
0
-0
/
+0
|
|
\
\
\
|
|
*
|
|
xorimm
submission_OOPSLA2021_RISCV
Léo Gourdin
2021-04-09
2
-0
/
+77
|
|
*
|
|
removing useless flag check
Léo Gourdin
2021-04-09
1
-3
/
+1
|
*
|
|
|
debug prints uniformized
Léo Gourdin
2021-05-18
1
-69
/
+66
|
*
|
|
|
for making the docker
David Monniaux
2021-05-11
4
-0
/
+3
[next]