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
/
backend
Commit message (
Expand
)
Author
Age
Files
Lines
*
Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...
David Monniaux
2020-03-03
68
-342
/
+4246
|
\
|
*
Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2
David Monniaux
2020-02-14
2
-4
/
+55
|
|
\
|
|
*
Added option -ftracelinearize which linearizes based on ifnot branches
Cyril SIX
2020-02-12
2
-4
/
+55
|
*
|
Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2
David Monniaux
2020-02-06
1
-3
/
+3
|
|
\
|
|
|
*
accessors for records are now not extracted it seems
David Monniaux
2020-02-06
1
-3
/
+3
|
*
|
Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2
David Monniaux
2020-02-06
3
-18
/
+593
|
|
\
|
|
|
*
Added flag to desactivate condition inversion
Cyril SIX
2020-02-03
1
-1
/
+2
|
|
*
Adding threshold to duplicate instructions
Cyril SIX
2020-01-31
1
-6
/
+12
|
|
*
Added debug message when inverting ifso ifnot
Cyril SIX
2020-01-24
1
-1
/
+3
|
|
*
Oracle inverting branches when trace does not go in fallthru
Cyril SIX
2020-01-24
1
-2
/
+21
|
|
*
Revert "Modified the hook for the oracle"
Cyril SIX
2020-01-23
3
-12
/
+8
|
|
*
Verificator finished for handling reversed Icond
Cyril SIX
2020-01-23
2
-11
/
+18
|
|
*
Added clause in match_inst to allow Icond reversal
Cyril SIX
2020-01-23
1
-4
/
+13
|
|
*
Modified the hook for the oracle
Cyril SIX
2020-01-23
3
-8
/
+12
|
|
*
Fixing bug caused by get_predecessors returning duplicates
Cyril SIX
2020-01-23
1
-5
/
+8
|
|
*
Printing traces right before duplicating
Cyril SIX
2020-01-23
1
-5
/
+2
|
|
*
Fixing bug (used physical instead of structural inequality)
Cyril SIX
2020-01-22
1
-1
/
+2
|
|
*
Merge branch 'mppa-work' into mppa-duplicate-oracle
Cyril SIX
2020-01-22
2
-0
/
+1134
|
|
|
\
|
|
*
|
Fixing is_empty function
Cyril SIX
2020-01-22
1
-3
/
+3
|
|
*
|
Branch duplication implementation
Cyril SIX
2020-01-22
1
-12
/
+94
|
|
*
|
Set up the groundbase for doing the duplication
Cyril SIX
2020-01-17
1
-4
/
+14
|
|
*
|
Removed unnecessary .mli file (provoked compilation problems)
Cyril SIX
2020-01-17
1
-12
/
+0
|
|
*
|
Adding more debug elements
Cyril SIX
2020-01-15
1
-1
/
+9
|
|
*
|
Typo in printf
Cyril SIX
2020-01-13
1
-1
/
+1
|
|
*
|
Opcode heuristic done for K1c
Cyril SIX
2019-12-16
2
-1
/
+3
|
|
*
|
Stub for opcode heuristic
Cyril SIX
2019-12-16
2
-4
/
+12
|
|
*
|
Fixing loop heuristic for the way CompCert handles loops
Cyril SIX
2019-12-11
1
-11
/
+19
|
|
*
|
Implemented call, return, store and loop heuristics
Cyril SIX
2019-12-11
1
-2
/
+55
|
|
*
|
Function to look ahead unconditionally
Cyril SIX
2019-12-11
1
-0
/
+12
|
|
*
|
Loop headers detection works!
Cyril SIX
2019-12-11
1
-3
/
+17
|
|
*
|
Dominators approach not working well ==> opting for visit approach
Cyril SIX
2019-12-10
1
-23
/
+73
|
|
*
|
Calcul de dominateurs a l'air de marcher
Cyril SIX
2019-12-10
1
-88
/
+144
|
|
*
|
Merge remote-tracking branch 'refs/remotes/origin/mppa-duplicate-oracle' into...
Cyril SIX
2019-12-09
4
-130
/
+11
|
|
|
\
\
|
|
|
*
\
Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-dupl...
David Monniaux
2019-12-09
4
-130
/
+11
|
|
|
|
\
\
|
|
*
|
|
|
Rajout du calcul de dominateurs - pas testé
Cyril SIX
2019-12-09
1
-16
/
+43
|
|
|
/
/
/
|
|
*
|
|
merge w/ non trapping loads
David Monniaux
2019-12-06
1
-3
/
+3
|
|
*
|
|
Merge remote-tracking branch 'origin/mppa-work' into mppa-duplicate-oracle
David Monniaux
2019-12-06
58
-423
/
+1502
|
|
|
\
\
\
|
|
*
|
|
|
Adding breadth first search
Cyril SIX
2019-12-06
1
-3
/
+6
|
|
*
|
|
|
[BROKEN] Compiles, not tested
Cyril SIX
2019-12-06
1
-3
/
+3
|
|
*
|
|
|
[BROKEN] Started BFS - does not compile
Cyril SIX
2019-12-05
1
-0
/
+30
|
|
*
|
|
|
bfs --> dfs
Cyril SIX
2019-12-05
1
-24
/
+26
|
|
*
|
|
|
Traces now stop at Icall/Ibuiltin/Ijumptable
Cyril SIX
2019-12-04
1
-6
/
+11
|
|
*
|
|
|
Fixed trace selection - for now, it only prints them, and the chosen paths ar...
Cyril SIX
2019-12-02
1
-17
/
+32
|
|
*
|
|
|
[BROKEN] Implementing trace selection from Chang & Hwu 1988, to be debugged
Cyril SIX
2019-10-09
1
-2
/
+163
|
*
|
|
|
|
CSE2 with NOTRAP
David Monniaux
2020-02-03
2
-95
/
+186
|
*
|
|
|
|
NOTRAP in CSE2: progress
David Monniaux
2020-02-03
2
-33
/
+260
|
*
|
|
|
|
Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert/dm-cse2 into mppa-cse2
David Monniaux
2020-02-03
1
-18
/
+18
|
|
\
\
\
\
\
|
*
\
\
\
\
\
Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert/dm-cse2 into mppa-cse2
David Monniaux
2020-02-03
2
-0
/
+14
|
|
\
\
\
\
\
\
|
*
\
\
\
\
\
\
Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2
David Monniaux
2020-01-28
2
-0
/
+1834
|
|
\
\
\
\
\
\
\
|
|
|
_
|
_
|
_
|
_
|
_
|
/
|
|
/
|
|
|
|
|
|
|
*
|
|
|
|
|
|
FINISHED the forward-moves pass
David Monniaux
2020-01-09
1
-2
/
+6
[next]