Commits · e37d655db0ec3d2c002e200c3e70a1997e39a458 · CertiCompil / CompCert-KVX

09 Apr, 2021 6 commits
- removing unusued proof line · e37d655d
  Léo Gourdin authored Apr 09, 2021
  
  e37d655d
- adding missing xorimm exp · 77f3fd97
  Léo Gourdin authored Apr 09, 2021
  
  77f3fd97
- Merge branch 'riscv-work' into kvx-work · b3009fc0
  Léo Gourdin authored Apr 09, 2021
  
  b3009fc0
- Remove flags · b0252257
  Léo Gourdin authored Apr 09, 2021
  
  b0252257
- Removing expansions from Asmgen · 18312f04
  Léo Gourdin authored Apr 09, 2021
  
  18312f04
- Removing addptrofs draft, next will be merging · b7720bc5
  Léo Gourdin authored Apr 09, 2021
  
  b7720bc5
08 Apr, 2021 1 commit
- bugfix · 2f2e7b1d
  Léo Gourdin authored Apr 08, 2021
  
  2f2e7b1d
06 Apr, 2021 1 commit
- Important commit on expansions' mini CSE, and a draft for addptrofs · dd4767e1
  Léo Gourdin authored Apr 06, 2021
  
  dd4767e1
30 Mar, 2021 3 commits
- a more general way to manage special registers before introducing SP · df9aab80
  Léo Gourdin authored Mar 30, 2021
  
  df9aab80
- Now a more general way to perform imm operations · 83b556a1
  Léo Gourdin authored Mar 30, 2021
  
  83b556a1
- Refactoring the mayundef OP to be more general... · 0d98d7fe
  Léo Gourdin authored Mar 30, 2021
  
  0d98d7fe
29 Mar, 2021 1 commit
- adding test for load replacement on a64 · 706b6384
  Léo Gourdin authored Mar 29, 2021
  
  706b6384
26 Mar, 2021 4 commits
- bugfix and printOp · 17b35c46
  Léo Gourdin authored Mar 26, 2021
  
  17b35c46
- fix admit · bc865be2
  Léo Gourdin authored Mar 26, 2021
  
  bc865be2
- Compiler options to manage expansions · 63ddeebc
  Léo Gourdin authored Mar 26, 2021
  
  63ddeebc
- Adding more expansions, improving miniCSE, and tuning prepass · 95205e72
  Léo Gourdin authored Mar 26, 2021
  
  95205e72
23 Mar, 2021 1 commit
- Bugfix liveness · ca78138a
  Léo Gourdin authored Mar 23, 2021
  
  ca78138a
21 Mar, 2021 1 commit
- Remove first nop when doing expansion · 21d43bc4
  Léo Gourdin authored Mar 21, 2021
  
  21d43bc4
10 Mar, 2021 1 commit
- fp test · bc4a980b
  Léo Gourdin authored Mar 10, 2021
  
  bc4a980b
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 1 commit
- [Admitted checker] Some more proof, version with buggy addirw0 · 8fb2a5a1
  Léo Gourdin authored Feb 25, 2021
  
  8fb2a5a1