| Commit message (Collapse) | Author | Age | Files | Lines | ||
|---|---|---|---|---|---|---|
| ... | ||||||
| | * | | Adding missing operators in PrintOp for debugging | Léo Gourdin | 2021-02-25 | 1 | -0/+5 | |
| | | | | ||||||
| | * | | écrase X31riscV-cmov | David Monniaux | 2021-02-03 | 1 | -1/+2 | |
| | | | | ||||||
| | * | | Merge remote-tracking branch 'origin/kvx-work' into riscV-cmov | David Monniaux | 2021-02-03 | 1 | -1/+1 | |
| | |\ \ | ||||||
| | * | | | no branchless by default | David Monniaux | 2021-02-02 | 1 | -1/+1 | |
| | | | | | ||||||
| | * | | | detect redundant cmov | David Monniaux | 2021-02-02 | 2 | -3/+34 | |
| | | | | | ||||||
| | * | | | fix code generation for select(b, r, r) | David Monniaux | 2021-02-02 | 1 | -2/+7 | |
| | | | | | ||||||
| | * | | | fix problem if rt = rf | David Monniaux | 2021-02-02 | 1 | -6/+8 | |
| | | | | | ||||||
| | * | | | example of cmov | David Monniaux | 2021-02-02 | 1 | -0/+28 | |
| | | | | | ||||||
| | * | | | Cmov Tsingle | David Monniaux | 2021-02-02 | 3 | -33/+43 | |
| | | | | | ||||||
| | * | | | implement for another register configuration | David Monniaux | 2021-02-02 | 1 | -1/+8 | |
| | | | | | ||||||
| | * | | | make branchless the default | David Monniaux | 2021-02-02 | 1 | -1/+1 | |
| | | | | | ||||||
| | * | | | some more cases implemented | David Monniaux | 2021-02-02 | 1 | -12/+25 | |
| | | | | | ||||||
| | * | | | Pselectd | David Monniaux | 2021-02-02 | 3 | -0/+33 | |
| | | | | | ||||||
| | * | | | cmov on integers | David Monniaux | 2021-02-02 | 3 | -11/+110 | |
| | | | | | ||||||
| | * | | | begin synthesizing select | David Monniaux | 2021-02-02 | 3 | -2/+34 | |
| | | | | | ||||||
| | * | | | asmgen Oselectl | David Monniaux | 2021-02-02 | 2 | -0/+11 | |
| | | | | | ||||||
| | * | | | begin implementing select | David Monniaux | 2021-02-02 | 8 | -6/+114 | |
| | | | | | ||||||
| | * | | | select01_long | David Monniaux | 2021-02-01 | 1 | -130/+10 | |
| | | | | | ||||||
| | * | | | repr etc. | David Monniaux | 2021-02-01 | 1 | -4/+2 | |
| | | | | | ||||||
| | * | | | bitwise_select_value_correct | David Monniaux | 2021-02-01 | 1 | -0/+12 | |
| | | | | | ||||||
| | * | | | int64_of_value some more | David Monniaux | 2021-02-01 | 1 | -14/+15 | |
| | | | | | ||||||
| | * | | | int64_of_value | David Monniaux | 2021-02-01 | 1 | -0/+77 | |
| | | | | | ||||||
| | * | | | Asmgen for bits / float | David Monniaux | 2021-02-01 | 1 | -0/+13 | |
| | | | | | ||||||
| | * | | | bits to float | David Monniaux | 2021-02-01 | 9 | -5/+82 | |
| | | | | | ||||||
| | * | | | fix Makefile / configure | David Monniaux | 2021-02-01 | 1 | -0/+6 | |
| | | | | | ||||||
| | * | | | adding builtins | David Monniaux | 2021-02-01 | 4 | -6/+27 | |
| | | | | | ||||||
| | * | | | Obits_of_single etc | David Monniaux | 2021-02-01 | 3 | -3/+46 | |
| | | | | | ||||||
| | * | | | define some semantics in Asm | David Monniaux | 2021-02-01 | 2 | -3/+24 | |
| | | | | | ||||||
| | * | | | add has_type info | David Monniaux | 2021-01-31 | 1 | -1/+3 | |
| | | | | | ||||||
| | * | | | has_type_b | David Monniaux | 2021-01-30 | 1 | -0/+21 | |
| | | | | | ||||||
| | * | | | select_long | David Monniaux | 2021-01-30 | 1 | -0/+38 | |
| | | | | | ||||||
| | * | | | select through bitwise operations | David Monniaux | 2021-01-30 | 1 | -0/+40 | |
| | | |/ | |/| | ||||||
| * | | | Try to save values in virtual registers during expansion | Léo Gourdin | 2021-03-01 | 3 | -95/+118 | |
| | | | | ||||||
| * | | | Proofs finished for expansion | Léo Gourdin | 2021-03-01 | 3 | -41/+68 | |
| | | | | ||||||
| * | | | Debugging fake values finished | Léo Gourdin | 2021-03-01 | 3 | -24/+39 | |
| | | | | ||||||
| * | | | proof of fsval_proj_correct | Sylvain Boulmé | 2021-03-01 | 1 | -7/+27 | |
| | | | | ||||||
| * | | | Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work | Léo Gourdin | 2021-03-01 | 1 | -4/+4 | |
| |\ \ \ | ||||||
| | * | | | bug fix ? | Sylvain Boulmé | 2021-03-01 | 1 | -4/+4 | |
| | | | | | ||||||
| * | | | | some bugfix | Léo Gourdin | 2021-03-01 | 2 | -15/+20 | |
| | | | | | ||||||
| * | | | | Proof of fsval condition cmp ok | Léo Gourdin | 2021-03-01 | 9 | -1138/+545 | |
| | | | | | ||||||
| * | | | | [Admitted checker] Some more proof, version with buggy addirw0 | Léo Gourdin | 2021-02-25 | 2 | -23/+128 | |
| | | | | | ||||||
| * | | | | some more proof for fake hsval checker expansions | Léo Gourdin | 2021-02-25 | 3 | -370/+772 | |
| | | | | | ||||||
| * | | | | [Intermediate] Adding fake hsval for Ccomp expansion | Léo Gourdin | 2021-02-23 | 4 | -171/+180 | |
| | | | | | ||||||
| * | | | | Fix imports | Léo Gourdin | 2021-02-23 | 1 | -1/+1 | |
| | | | | | ||||||
| * | | | | Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work | Léo Gourdin | 2021-02-23 | 9 | -80/+223 | |
| |\| | | | ||||||
| | * | | | Merge branch 'riscv-work-rules' of ↵ | Léo Gourdin | 2021-02-23 | 1 | -2/+52 | |
| | |\ \ \ | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into riscv-work-rules | |||||
| | | * | | | add target_cbranch_expanse | Sylvain Boulmé | 2021-02-23 | 1 | -2/+52 | |
| | | | | | | ||||||
| | * | | | | Separate target_op_simplify for riscV | Léo Gourdin | 2021-02-23 | 3 | -19/+22 | |
| | |/ / / | ||||||
| | * | | | fix comments | Sylvain Boulmé | 2021-02-23 | 1 | -2/+5 | |
| | | | | | ||||||
| | * | | | starting an interface for target rewriting rules. | Sylvain Boulmé | 2021-02-23 | 1 | -9/+130 | |
| | | | | | ||||||
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |