Commits · 916cdf939e6f76c2729f123c40c0a10bb63bcd60 · CertiCompil / CompCert-KVX

30 Jan, 2019 10 commits
- long types are 8 bytes now · 916cdf93
  Cyril SIX authored Jan 30, 2019
  
  916cdf93
- same format as the others · 472a0e03
  David Monniaux authored Jan 30, 2019
  
  472a0e03
- bitsliced TEA from archived http://plaintext.crypto.lo.gy/article/378/untwisted-bit-sliced-tea-time · b8a398d3
  David Monniaux authored Jan 30, 2019
  
  b8a398d3
- correct path to ccomp · db17026d
  David Monniaux authored Jan 30, 2019
  
  db17026d
- https://github.com/conorpp/bitsliced-aes · 3e6decf9
  David Monniaux authored Jan 30, 2019
  
  3e6decf9
- fixes in makefiles · 07f94da0
  David Monniaux authored Jan 30, 2019
  
  07f94da0
- synchronized with David's scheduling work · a5da25f1
  David Monniaux authored Jan 30, 2019
  
  a5da25f1
- the state of things that work · f48c84ca
  David Monniaux authored Jan 30, 2019
  
  f48c84ca
- blowfish · 09341d6d
  David Monniaux authored Jan 30, 2019
  
  09341d6d
- remove workaround · a50e263c
  David Monniaux authored Jan 30, 2019
  
  a50e263c
29 Jan, 2019 10 commits
- no need for this anymore · 258b9942
  David Monniaux authored Jan 29, 2019
  
  258b9942
- https://github.com/pfalcon/uzlib · 417b4381
  David Monniaux authored Jan 29, 2019
  
  417b4381
- muf muf muf · 15aafbb6
  David Monniaux authored Jan 29, 2019
  
  15aafbb6
- jpeg-6b modified · c92fb6be
  David Monniaux authored Jan 29, 2019
  
  c92fb6be
- give meaningful "unhandled instr" messages · 295ea9f5
  David Monniaux authored Jan 29, 2019
  
  295ea9f5
- Merge branch 'mppa_postpass' of... · 6ff3de98
  David Monniaux authored Jan 29, 2019
```
Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
```
  6ff3de98
- Adding indirect calls (icall instruction) · 0a693ac9
  Cyril SIX authored Jan 25, 2019
  
  0a693ac9
- Hypothèses de pc_set_add permettant de prouver le lemme · 61bd09ba
  Cyril SIX authored Jan 29, 2019
  
  61bd09ba
- Avancement sur exec_basic_instr_pcvar + exec_load et exec_store prennent des ireg au lieu de preg · ba51ef8f
  Cyril SIX authored Jan 28, 2019
  
  ba51ef8f
- ça make · 734a3fee
  David Monniaux authored Jan 29, 2019
  
  734a3fee
28 Jan, 2019 1 commit
- crypto algorithms from https://github.com/B-Con/crypto-algorithms/ · 253446c2
  David Monniaux authored Jan 28, 2019
  
  253446c2
27 Jan, 2019 3 commits
- give meaningful messages please · 88a8995f
  David Monniaux authored Jan 27, 2019
  
  88a8995f
- packaged · b0b62fc1
  David Monniaux authored Jan 27, 2019
  
  b0b62fc1
- picosat · 4ef8259d
  David Monniaux authored Jan 27, 2019
```
induces bug in register allocation
```
  4ef8259d
26 Jan, 2019 4 commits
- to test · c6fd1131
  David Monniaux authored Jan 26, 2019
  
  c6fd1131
- clock cycles etc. · 47165c52
  David Monniaux authored Jan 26, 2019
  
  47165c52
- micro bunzip · 86629431
  David Monniaux authored Jan 26, 2019
  
  86629431
- micro bunzip · 2dfb8329
  David Monniaux authored Jan 26, 2019
  
  2dfb8329
25 Jan, 2019 4 commits
- Merge branch 'mppa_postpass' of... · 9ac6ffec
  David Monniaux authored Jan 25, 2019
```
Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
```
  9ac6ffec
- Avancement PostpassSchedulingproof · e61639d9
  Cyril SIX authored Jan 25, 2019
  
  e61639d9
- Merge branch 'mppa_postpass' of... · 6a2030b3
  Cyril SIX authored Jan 25, 2019
```
Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass

Conflicts:
	mppa_k1c/PostpassSchedulingproof.v
```
  6a2030b3
- Progrès dans PostpassSchedulingproof · 0e208091
  Cyril SIX authored Jan 25, 2019
  
  0e208091
24 Jan, 2019 2 commits
- Merge branch 'mppa_postpass' of... · 02d713c1
  David Monniaux authored Jan 24, 2019
```
Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
```
  02d713c1
- Un peu d'avancement sur PostpassSchedulingproof · e83e5989
  Cyril SIX authored Jan 24, 2019
  
  e83e5989
23 Jan, 2019 6 commits
- Merge branch 'mppa_postpass' of... · 3ccbf97b
  David Monniaux authored Jan 23, 2019
```
Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
```
  3ccbf97b
- Preuve de app_nonil2 dans PostpassSchedulingproof · ee8a92ea
  Cyril SIX authored Jan 23, 2019
  
  ee8a92ea
- Cleaning dans PostpassSchedulingproof · 897d83b8
  Cyril SIX authored Jan 23, 2019
  
  897d83b8
- 3ème cas de transf_step_correct de PostpassSchedulingproof fini · 644aaedd
  Cyril SIX authored Jan 23, 2019
  
  644aaedd
- Proof of builtin case for transf_step_correct in PostpassSchedulingproof · 463bcb7f
  Cyril SIX authored Jan 23, 2019
  
  463bcb7f
- Adding a predicate that a builtin must be alone in its basicblock · afe2e1eb
  Cyril SIX authored Jan 23, 2019
  
  afe2e1eb