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
...
*
|
Enlevé la dépendance mémoire de Pcbu
Cyril SIX
2019-03-13
3
-25
/
+25
*
|
for scip
David Monniaux
2019-03-13
1
-0
/
+11
*
|
for using CPlex
David Monniaux
2019-03-13
2
-5
/
+19
*
|
scripts for using Gurobi and Cplex for ILP solving
David Monniaux
2019-03-13
2
-2
/
+2
*
|
attempt at parser for cplex
David Monniaux
2019-03-13
1
-0
/
+7
*
|
-fpostpass-ilp
David Monniaux
2019-03-12
5
-16
/
+3
*
|
script for using Gurobi with -fpostpass-ilp
David Monniaux
2019-03-12
1
-0
/
+3
*
|
Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...
David Monniaux
2019-03-12
5
-110
/
+141
|
\
\
|
*
|
Added cascaded_scheduler but the flag does not work
Cyril SIX
2019-03-12
2
-3
/
+4
|
*
|
Added a flag for changing the scheduler (not any choice available right now)
Cyril SIX
2019-03-12
5
-3
/
+12
|
*
|
Proof of exec_trans_pcincr solved
Cyril SIX
2019-03-12
1
-7
/
+31
|
*
|
Merge remote-tracking branch 'origin/mppa_parcheck' into mppa_parcheck
Cyril SIX
2019-03-12
1
-12
/
+12
|
|
\
\
|
|
*
|
fix trans_pcincr for parcheck. (Proof is broken. cf FIXME)
Sylvain Boulmé
2019-03-12
1
-12
/
+12
|
*
|
|
Simplification des preuves "de discrimination" dans Asmblockdeps
Cyril SIX
2019-03-12
1
-94
/
+77
|
|
/
/
|
*
|
[BROKEN] Added parallelizability check - breaks all the conditional jumps
Cyril SIX
2019-03-12
2
-1
/
+19
*
|
|
-fpostpass-ilp
David Monniaux
2019-03-12
3
-2
/
+7
*
|
|
better tracing for ILP + make clean
David Monniaux
2019-03-12
3
-3
/
+12
*
|
|
Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...
David Monniaux
2019-03-12
1
-5
/
+10
|
\
|
|
|
*
|
Fix for frame pointer being destroyed
Cyril SIX
2019-03-12
1
-5
/
+10
*
|
|
forgot a free()
David Monniaux
2019-03-12
1
-0
/
+1
*
|
|
simpler Makefiles
David Monniaux
2019-03-12
1
-0
/
+12
|
/
/
*
|
et hop un Makefile pour les matrices complexes
David Monniaux
2019-03-12
2
-0
/
+12
*
|
some more optimized complex matrix
David Monniaux
2019-03-12
1
-12
/
+9
*
|
easier for clocking directly from ccomp files
David Monniaux
2019-03-12
2
-0
/
+5
*
|
some more work on complex matrices
David Monniaux
2019-03-12
1
-8
/
+195
*
|
some more about complex numbers
David Monniaux
2019-03-11
1
-8
/
+49
*
|
wrong directory, fixed
David Monniaux
2019-03-11
1
-0
/
+0
*
|
et hop un Makefile
David Monniaux
2019-03-11
1
-0
/
+9
*
|
complex numbers attempt
David Monniaux
2019-03-10
1
-0
/
+22
*
|
test code for jump tables
David Monniaux
2019-03-10
1
-0
/
+34
*
|
varargs
David Monniaux
2019-03-10
2
-18
/
+2
*
|
forgot the Makefile
David Monniaux
2019-03-10
1
-0
/
+18
*
|
test for volatiles
David Monniaux
2019-03-10
1
-0
/
+33
*
|
volatile stores
David Monniaux
2019-03-10
3
-45
/
+42
*
|
volatile load
David Monniaux
2019-03-10
1
-37
/
+37
*
|
demo for volatile
David Monniaux
2019-03-09
2
-9
/
+28
*
|
program for testing volatiles
David Monniaux
2019-03-09
1
-0
/
+32
*
|
store the assembly source code as well
David Monniaux
2019-03-09
1
-5
/
+8
*
|
code qui plante
David Monniaux
2019-03-08
3
-0
/
+33
*
|
Modified test/c/Makefile for CompCert tests (remove all the float tests with ...
Cyril SIX
2019-03-08
2
-5
/
+6
*
|
Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...
David Monniaux
2019-03-08
1
-0
/
+1
|
\
\
|
*
|
Added error message for Odivfs in Asmblockgen
Cyril SIX
2019-03-08
1
-0
/
+1
*
|
|
un example avec varargs flottants
David Monniaux
2019-03-08
1
-0
/
+34
|
/
/
*
|
disable useless warnings
David Monniaux
2019-03-08
4
-4
/
+4
*
|
Rajout de commentaires sur les instructions non émises
Cyril SIX
2019-03-08
1
-8
/
+8
*
|
Fix for the compw immediate problem
Cyril SIX
2019-03-08
1
-7
/
+17
*
|
Minor fix on TargetPrinter (coqint instead of coqint64 for adequate types)
Cyril SIX
2019-03-08
1
-8
/
+8
*
|
Refactorisation des load et des store
Cyril SIX
2019-03-08
3
-62
/
+40
*
|
Reverting the hack introduces on Pcompw etc..
Cyril SIX
2019-03-08
1
-14
/
+3
*
|
Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patch
Cyril SIX
2019-03-08
9
-45
/
+394
|
\
\
[prev]
[next]