Commits · a19d458fc0760a10fb42fdbcdd3ba92ec3aa3e83 · CertiCompil / CompCert-KVX

28 Aug, 2020 2 commits
- SUCCESS: prouve 1 des admit de hsistate_simu_core_correct. · a19d458f
  Sylvain Boulmé authored Aug 28, 2020
```
Le deuxième doit marcher à peu près pareil modulo siexits_simu_all_fallthrough_upto à corriger ?
```
  a19d458f
- add nested_sok in hsistate_refines_dyn · 09e5f05e
  Sylvain Boulmé authored Aug 28, 2020
```
and proves preservation of refinement
```
  09e5f05e
27 Aug, 2020 2 commits
- more realistic ok_allexit. · ca64d933
  Sylvain Boulmé authored Aug 27, 2020
  
  ca64d933
- reduction de la preuve de raffinement du exit à ok_allexit · 1b196baa
  Sylvain Boulmé authored Aug 27, 2020
  
  1b196baa
26 Aug, 2020 8 commits
- proof of lemma hslocal_set_sreg_correct · 5888db3a
  Sylvain Boulmé authored Aug 26, 2020
  
  5888db3a
- simplification of hsilocal_refines · 8e92380a
  Sylvain Boulmé authored Aug 26, 2020
  
  8e92380a
- starting hslocal_set_sreg_correct · 0bb94207
  Sylvain Boulmé authored Aug 26, 2020
  
  0bb94207
- Comment change · 15a804f7
  Cyril SIX authored Aug 26, 2020
  
  15a804f7
- Merge branch 'mppa-RTLpathSE-verif' of... · 3f0b5b50
  Sylvain Boulmé authored Aug 26, 2020
```
Merge branch 'mppa-RTLpathSE-verif' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-verif
```
  3f0b5b50
- fix statement of hslocal_set_sreg_correct ? · db8d42bd
  Sylvain Boulmé authored Aug 26, 2020
  
  db8d42bd
- Avancement divers · 47217508
  Cyril SIX authored Aug 26, 2020
  
  47217508
- simplify hsi_lsmem into hsi_smem · f322d525
  Sylvain Boulmé authored Aug 26, 2020
  
  f322d525
25 Aug, 2020 2 commits
- Start of hfinal_simu_core_correct · 58408dcb
  Cyril SIX authored Aug 25, 2020
  
  58408dcb
- hfinal_refines depend on ge, sp, rs0, m0 · bc9aefec
  Cyril SIX authored Aug 25, 2020
  
  bc9aefec
24 Aug, 2020 3 commits
- Down to hsexec_final_correct · c5dabaf9
  Cyril SIX authored Aug 24, 2020
  
  c5dabaf9
- Simpler hypothesis · 2010c5aa
  Cyril SIX authored Aug 24, 2020
  
  2010c5aa
- Avancement sur simu_check_single_correct · a7e62465
  Cyril SIX authored Aug 24, 2020
  
  a7e62465
21 Aug, 2020 1 commit
- Avancement · 5e47c496
  Cyril SIX authored Aug 21, 2020
  
  5e47c496
20 Aug, 2020 1 commit
- Started to port the properties from RTLpathSE_impl.v · 165f996b
  Cyril SIX authored Aug 20, 2020
  
  165f996b
19 Aug, 2020 2 commits
- Pushed by mistake on runtime/include/ccomp_kvx_fixes.h · 47f0ea6c
  Cyril SIX authored Aug 19, 2020
  
  47f0ea6c
- Merge remote-tracking branch 'origin/mppa-RTLpathSE-verif-hash-junk' into mppa-RTLpathSE-verif · 7c2c4694
  Cyril SIX authored Aug 19, 2020
  
  7c2c4694
18 Aug, 2020 7 commits
- Fixing proofs - back to being able to build · f05d3092
  Cyril SIX authored Aug 18, 2020
  
  f05d3092
- Propagating changes to hsistate_simu_core_correct · bd49d137
  Cyril SIX authored Aug 18, 2020
  
  bd49d137
- Changing siexit_simu to be able to prove hsiexit_simu_core_correct · a4f14d0a
  Cyril SIX authored Aug 18, 2020
```
Hopefully it's a good change?
```
  a4f14d0a
- One part of hsiexit_simu_core_correct · 3fb75591
  Cyril SIX authored Aug 18, 2020
  
  3fb75591
- Proof of hsilocal_simu_core_correct · d83fe02d
  Cyril SIX authored Aug 18, 2020
  
  d83fe02d
- None case · b2ccbc03
  Cyril SIX authored Aug 18, 2020
  
  b2ccbc03
- Using PTree.combine to express picking register values from either rs0 or hst · 382c23c7
  Cyril SIX authored Aug 18, 2020
  
  382c23c7
17 Aug, 2020 1 commit
- Trying to modify definitions to include list of alive registers · d04dc09c
  Cyril SIX authored Aug 17, 2020
  
  d04dc09c
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