| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Adding fp init expansions | Léo Gourdin | 2021-03-02 | 1 | -0/+15 |
| * | Proofs finished for expansion | Léo Gourdin | 2021-03-01 | 1 | -18/+61 |
| * | Debugging fake values finished | Léo Gourdin | 2021-03-01 | 1 | -7/+14 |
| * | some bugfix | Léo Gourdin | 2021-03-01 | 1 | -11/+16 |
| * | Proof of fsval condition cmp ok | Léo Gourdin | 2021-03-01 | 1 | -91/+389 |
| * | [Admitted checker] Some more proof, version with buggy addirw0 | Léo Gourdin | 2021-02-25 | 1 | -5/+126 |
| * | some more proof for fake hsval checker expansions | Léo Gourdin | 2021-02-25 | 1 | -44/+769 |
| * | [Intermediate] Adding fake hsval for Ccomp expansion | Léo Gourdin | 2021-02-23 | 1 | -3/+108 |
| * | Separate target_op_simplify for riscV | Léo Gourdin | 2021-02-23 | 1 | -0/+19 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |