Commits · v3.8_kvx · CertiCompil / Chamois-Arsene

Dec 07, 2020
- Fixing test/regression for KVX · 23da7b35
  Cyril SIX authored 4 years ago
  
  View commits for tag v3.8_kvx v3.8_kvx
  
  23da7b35
Dec 04, 2020
- Merge branch 'kvx-work' into kvx-work-merge3.8 · 60ff1e39
  Cyril SIX authored 4 years ago
  60ff1e39
- Fixing compilation for KVX · f2fb8540
  Cyril SIX authored 4 years ago
  
  f2fb8540
- Comment · d2197102
  Cyril SIX authored 4 years ago
  
  d2197102
- Less aggressive tail duplication · 718a7da9
  Cyril SIX authored 4 years ago
  718a7da9
- Clean-up debug · 2bbb2af7
  Cyril SIX authored 4 years ago
  
  2bbb2af7
- Fixed infinite loop on find_last_node_before_loop · 079fe685
  Cyril SIX authored 4 years ago
  079fe685
Dec 03, 2020
- still issues with FR in kvx · 2d41078f
  David Monniaux authored 4 years ago
  
  2d41078f
- some fixes for KVX · 48dc0300
  David Monniaux authored 4 years ago
  
  48dc0300
Dec 02, 2020
- Slight perf improvement · abae3de5
  Cyril SIX authored 4 years ago
  
  abae3de5
- [expensive] Behavior change when the loop has two final instructions · ed8aec9f
  Cyril SIX authored 4 years ago
  ed8aec9f
Dec 01, 2020
- Duplicateaux: Generalization of look_ahead · 73729e86
  Cyril SIX authored 4 years ago
  
  73729e86
- Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass · 035a1a9f
  Cyril SIX authored 4 years ago
  035a1a9f
- Ignore loopback edges on tail-duplicate · 790161a5
  Cyril SIX authored 4 years ago
  
  790161a5
Nov 25, 2020
- store2_sound · b8647d11
  David Monniaux authored 4 years ago
  
  b8647d11
- clever_kill_store_sound · e856fe63
  David Monniaux authored 4 years ago
  
  e856fe63
- kill_store_sound · a49044a6
  David Monniaux authored 4 years ago
  
  a49044a6
- two lemmas admitted · 0b76b98f
  David Monniaux authored 4 years ago
  
  0b76b98f
- missing lemmas · 38f279e6
  David Monniaux authored 4 years ago
  
  38f279e6
- pointer_eq copied · 2a579bf4
  David Monniaux authored 4 years ago
  
  2a579bf4
Nov 24, 2020
- Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass · 43a7cc2a
  David Monniaux authored 4 years ago
  
  43a7cc2a
- tiny simplification in Tunnelingaux.ml · a9677e17
  Sylvain Boulmé authored 4 years ago
  
  a9677e17
Nov 23, 2020
- bug #223 fix on PPC · 1fc9e3b1
  David Monniaux authored 4 years ago
  
  1fc9e3b1
- bug #223 fix for ARM · 959c1084
  David Monniaux authored 4 years ago
  
  959c1084
- bug #223 fix on x86 / x86-64 · 7c63e3df
  David Monniaux authored 4 years ago
  
  7c63e3df
- fix wrong version of file on AArch64 · 893dba63
  David Monniaux authored 4 years ago
  
  893dba63
- Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work · ce7ba158
  David Monniaux authored 4 years ago
  
  ce7ba158
- fix bug #223 on AArch64 · c3114f51
  David Monniaux authored 4 years ago
  
  c3114f51
- fix bug #223 on Risc-V · d4f3b864
  David Monniaux authored 4 years ago
  
  d4f3b864
- correction bug #223 sur KVX · 36c82ee8
  David Monniaux authored 4 years ago
  
  36c82ee8
Nov 20, 2020
- prepass scheduling proof finished ! · c10f3ec4
  Sylvain Boulmé authored 4 years ago
  c10f3ec4
Nov 19, 2020
- merge nouveau tunneling · a0cc099c
  David Monniaux authored 4 years ago
  
  a0cc099c
- Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass · 193a466d
  David Monniaux authored 4 years ago
  
  193a466d
- fix Makefile pour kvx · 8bb9da51
  David Monniaux authored 4 years ago
  
  8bb9da51
- un peu de progrès sur le Makefile · 6d4b4810
  David Monniaux authored 4 years ago
  
  6d4b4810
- Asmgenproof1 pas sur kvx · 293e792b
  David Monniaux authored 4 years ago
  
  293e792b
- for 2010-11-18 Kalray release · 6d9f40cb
  David Monniaux authored 4 years ago
  
  6d9f40cb
- essai de limitation des paquets Kalray · 3ecf7822
  David Monniaux authored 4 years ago
  
  3ecf7822
- rm unneeded open statements in ML · 8457cd39
  David Monniaux authored 4 years ago
  
  8457cd39
- fix Makefile · 54146626
  David Monniaux authored 4 years ago
  
  54146626