Commits · 93f9aa39b2885f98bf2be89583102d5c7f4c6f22 · CertiCompil / CompCert-KVX

16 Sep, 2020 2 commits
- just missing OpWeights for AARCH64 · 93f9aa39
  David Monniaux authored Sep 16, 2020
  
  93f9aa39
- starting to move common files · 6e4f49f7
  David Monniaux authored Sep 16, 2020
  
  6e4f49f7
10 Sep, 2020 2 commits
- Merge branch 'mppa-RTLpathSE-verif-hash-junk' of... · 2e54a9c5
  David Monniaux authored Sep 10, 2020
```
Merge branch 'mppa-RTLpathSE-verif-hash-junk' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-verif-hash-junk
```
  2e54a9c5
- use with_destructor · 0566b93d
  David Monniaux authored Sep 10, 2020
  
  0566b93d
05 Sep, 2020 1 commit
- Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-verif-hash-junk · 8d1c157b
  David Monniaux authored Sep 05, 2020
```
iMe
```
  8d1c157b
02 Sep, 2020 2 commits
- remettre yarpgen · eafda94d
  David Monniaux authored Sep 02, 2020
  
  eafda94d
- fix issue 198 (incorrect reservation table for multiply-add) · 4ad441ab
  David Monniaux authored Sep 02, 2020
  
  4ad441ab
01 Sep, 2020 1 commit
- "nop" is not even printed out and thus uses no resources · 93604827
  David Monniaux authored Sep 01, 2020
  
  93604827
31 Aug, 2020 3 commits
- example prog where list scheduler can be reoptimized using ILP · df762ec0
  David Monniaux authored Aug 31, 2020
  
  df762ec0
- clean solution to close channels · 554eee04
  David Monniaux authored Aug 31, 2020
  
  554eee04
- fix problem with some file descriptors possibly never getting closed · 6f12f83d
  David Monniaux authored Aug 31, 2020
```
(need to propagate fix to other kinds of solvers)
```
  6f12f83d
31 Jul, 2020 2 commits
- links to the impure library on github · e069f9ab
  Sylvain Boulmé authored Jul 31, 2020
  
  e069f9ab
- Improving Coqdoc on abstractbb · fd09c489
  Sylvain Boulmé authored Jul 31, 2020
  
  fd09c489
30 Jul, 2020 2 commits
- -ftracelinearize · d1a06a9c
  David Monniaux authored Jul 30, 2020
  
  d1a06a9c
- Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-verif-hash-junk · e9e02812
  David Monniaux authored Jul 30, 2020
  
  e9e02812
29 Jul, 2020 1 commit
- Improving the coqdoc · 2e39ecb4
  Sylvain Boulmé authored Jul 29, 2020
  
  2e39ecb4
28 Jul, 2020 8 commits
- reinstate TARGET_CC · 1bb219c2
  David Monniaux authored Jul 28, 2020
  
  1bb219c2
- rm mods for running tests · a1c113c4
  David Monniaux authored Jul 28, 2020
  
  a1c113c4
- kvx-work now has CI automatically · 064e0f7b
  David Monniaux authored Jul 28, 2020
  
  064e0f7b
- do not use all-loads-nontrap · 3a4e2750
  David Monniaux authored Jul 28, 2020
  
  3a4e2750
- let's try directly OCaml 4.09.1 · e60a7329
  David Monniaux authored Jul 28, 2020
  
  e60a7329
- try to get gitlab-CI to use Coq 8.11.2 not 8.12 · 7c2962e1
  David Monniaux authored Jul 28, 2020
  
  7c2962e1
- fix Coq to 8.11.2 for CI · 14ce1b03
  David Monniaux authored Jul 28, 2020
  
  14ce1b03
- AUXR · 760015df
  David Monniaux authored Jul 28, 2020
  
  760015df
27 Jul, 2020 1 commit

Merge branch 'mppa-RTLpathSE-verif-hash-junk' of... · 8cee2111

David Monniaux authored Jul 27, 2020

Merge branch 'mppa-RTLpathSE-verif-hash-junk' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-verif-hash-junk

8cee2111

26 Jul, 2020 7 commits
- test for speculative load · d2a72d92
  David Monniaux authored Jul 26, 2020
  
  d2a72d92
- simplified · aa9060d7
  David Monniaux authored Jul 26, 2020
  
  aa9060d7
- cycle times · a643dc0d
  David Monniaux authored Jul 26, 2020
  
  a643dc0d
- Merge branch 'mppa-RTLpathSE-verif-hash-junk' of... · a7ba9012
  David Monniaux authored Jul 26, 2020
```
Merge branch 'mppa-RTLpathSE-verif-hash-junk' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-verif-hash-junk
```
  a7ba9012
- fix for coq · 373c56a4
  David Monniaux authored Jul 26, 2020
  
  373c56a4
- adapt filename · 17e3dbcf
  David Monniaux authored Jul 26, 2020
  
  17e3dbcf
- yet another attempt · 8d9cdaac
  David Monniaux authored Jul 26, 2020
  
  8d9cdaac
25 Jul, 2020 3 commits
- silly bug · ea70d7a4
  David Monniaux authored Jul 25, 2020
  
  ea70d7a4
- run some more valgrind in case of optimizations · dd28826f
  David Monniaux authored Jul 25, 2020
  
  dd28826f
- improved testcmp: detect maybe uninitialized · 4e89be4c
  David Monniaux authored Jul 25, 2020
  
  4e89be4c
24 Jul, 2020 5 commits
- > vs tee · 2ff9a87d
  David Monniaux authored Jul 24, 2020
  
  2ff9a87d
- for reducing · 01478f93
  David Monniaux authored Jul 24, 2020
  
  01478f93
- Coq 8.11.2 · 2fa48a42
  David Monniaux authored Jul 24, 2020
  
  2fa48a42
- picosat in one file for testing purposes · 9464136b
  David Monniaux authored Jul 24, 2020
  
  9464136b
- also crashes with 0 variables · cffd805e
  David Monniaux authored Jul 24, 2020
  
  cffd805e