Commits · d1d6493816e7c561f82f7549f100442f0bf52a15 · CertiCompil / CompCert-KVX

08 Mar, 2021 1 commit
- Adding miniCSE here too · d1d64938
  Léo Gourdin authored Mar 08, 2021
  
  d1d64938
06 Mar, 2021 3 commits
- Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexp · 0b402973
  Léo Gourdin authored Mar 06, 2021
  
  0b402973
- some simplification in miniCSE · 9882b342
  Léo Gourdin authored Mar 06, 2021
  
  9882b342
- Adding a mini CSE pass in the expansion oracle · c19ecc93
  Léo Gourdin authored Mar 06, 2021
  
  c19ecc93
02 Mar, 2021 8 commits
- Adding a flag to test fp_init_exp · eb35c300
  Léo Gourdin authored Mar 02, 2021
  
  eb35c300
- Adding fp init expansions · 6f71a2a3
  Léo Gourdin authored Mar 02, 2021
  
  6f71a2a3
- Merge remote-tracking branch 'origin/riscv-still-asmcondexp' into riscv-work-fpinit-stillexp · ef67224a
  Léo Gourdin authored Mar 02, 2021
  
  ef67224a
- [Admitted checker] Oracle expansion for float/float32 constant init · 801cd27e
  Léo Gourdin authored Mar 02, 2021
  
  801cd27e
- fix ci ? · 3e953ef4
  Léo Gourdin authored Mar 02, 2021
  
  3e953ef4
- Asmcondexp branche useful to benchmark expansions · 9bd7dcfb
  Léo Gourdin authored Mar 02, 2021
  
  9bd7dcfb
- Merge conflicts solved and cleaning in Asmgenproof after expansion · 6bff68d5
  Léo Gourdin authored Mar 02, 2021
  
  6bff68d5
- Merge remote-tracking branch 'origin/riscV-cmov' into riscv-work · be4dcbd9
  Léo Gourdin authored Mar 02, 2021
  
  be4dcbd9
01 Mar, 2021 8 commits
- Try to save values in virtual registers during expansion · fd1a0395
  Léo Gourdin authored Mar 01, 2021
  
  fd1a0395
- Proofs finished for expansion · dae202e1
  Léo Gourdin authored Mar 01, 2021
  
  dae202e1
- Debugging fake values finished · 9d0ae473
  Léo Gourdin authored Mar 01, 2021
  
  9d0ae473
- proof of fsval_proj_correct · d5ce8079
  Sylvain Boulmé authored Mar 01, 2021
  
  d5ce8079
- Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work · 9a0cf394
  Léo Gourdin authored Mar 01, 2021
  
  9a0cf394
- some bugfix · a3d782f1
  Léo Gourdin authored Mar 01, 2021
  
  a3d782f1
- bug fix ? · 221115bb
  Sylvain Boulmé authored Mar 01, 2021
  
  221115bb
- Proof of fsval condition cmp ok · 80db8e4b
  Léo Gourdin authored Mar 01, 2021
  
  80db8e4b
25 Feb, 2021 3 commits
- [Admitted checker] Some more proof, version with buggy addirw0 · 8fb2a5a1
  Léo Gourdin authored Feb 25, 2021
  
  8fb2a5a1
- some more proof for fake hsval checker expansions · c3bebbcc
  Léo Gourdin authored Feb 25, 2021
  
  c3bebbcc
- Adding missing operators in PrintOp for debugging · a9763cd4
  Léo Gourdin authored Feb 25, 2021
  
  a9763cd4
23 Feb, 2021 10 commits
- [Intermediate] Adding fake hsval for Ccomp expansion · 313443c8
  Léo Gourdin authored Feb 23, 2021
  
  313443c8
- Fix imports · 7bc14dbf
  Léo Gourdin authored Feb 23, 2021
  
  7bc14dbf
- Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work · a78fe0ef
  Léo Gourdin authored Feb 23, 2021
  
  a78fe0ef
- Merge branch 'riscv-work-rules' of... · 91699fd3
  Léo Gourdin authored Feb 23, 2021
```
Merge branch 'riscv-work-rules' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into riscv-work-rules
```
  91699fd3
- Separate target_op_simplify for riscV · 4192b5f4
  Léo Gourdin authored Feb 23, 2021
  
  4192b5f4
- add target_cbranch_expanse · 997d7f1a
  Sylvain Boulmé authored Feb 23, 2021
  
  997d7f1a
- fix comments · 9cddf911
  Sylvain Boulmé authored Feb 23, 2021
  
  9cddf911
- starting an interface for target rewriting rules. · 75a9af77
  Sylvain Boulmé authored Feb 23, 2021
  
  75a9af77
- others case for ccompimm · 3ce99d1f
  Léo Gourdin authored Feb 23, 2021
  
  3ce99d1f
- Some more proofs on branch expansion, using make_immed32_sound · e8322076
  Léo Gourdin authored Feb 23, 2021
  
  e8322076
22 Feb, 2021 2 commits
- improved pre_output_regs · 3b6a45c1
  Sylvain Boulmé authored Feb 22, 2021
  
  3b6a45c1
- a bit more cleaning · b0452edc
  Sylvain Boulmé authored Feb 22, 2021
  
  b0452edc
19 Feb, 2021 1 commit
- Branch expansions activated and configured in the checker (but admitted) and... · fb6325b4
  Léo Gourdin authored Feb 19, 2021
```
Branch expansions activated and configured in the checker (but admitted) and bugfix in the expansion liveness modification
```
  fb6325b4
18 Feb, 2021 1 commit
- Proof of Ocmp expansions without immediate and some drafts in comment · 9c9d516b
  Léo Gourdin authored Feb 18, 2021
  
  9c9d516b
16 Feb, 2021 3 commits
- quick fixcomments · 8faafc76
  Léo Gourdin authored Feb 16, 2021
  
  8faafc76
- fix bug in merge · 1e06ebb8
  Léo Gourdin authored Feb 16, 2021
  
  1e06ebb8
- Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-work · fe4d2149
  Léo Gourdin authored Feb 16, 2021
  
  fe4d2149