| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | rm condition parametrization in CSE3analysis | David Monniaux | 2021-07-16 | 1 | -5/+2 |
| * | begin implementing -fcse3-conditions | David Monniaux | 2020-12-09 | 1 | -4/+7 |
| * | CSE3 + conditions proof | David Monniaux | 2020-12-09 | 1 | -1/+24 |
| * | progress moving to list of items | David Monniaux | 2020-12-09 | 1 | -27/+23 |
| * | analysis with Abst_same | David Monniaux | 2020-12-08 | 1 | -15/+20 |
| * | CSE3 now runs on its own fixpoint iterator not based on Kildall.v | David Monniaux | 2020-12-08 | 1 | -0/+2 |
| * | is_condition_present_sound | David Monniaux | 2020-11-26 | 1 | -1/+6 |
| * | ajouté Cond, tout passe | David Monniaux | 2020-11-26 | 1 | -7/+9 |
| * | passage à Equ | David Monniaux | 2020-11-26 | 1 | -72/+61 |
| * | cond_valid_pointer_eq | David Monniaux | 2020-11-25 | 1 | -0/+14 |
| * | two lemmas admitted | David Monniaux | 2020-11-25 | 1 | -2/+20 |
| * | refixcse3 | David Monniaux | 2020-11-03 | 1 | -16/+29 |
| * | seems to work better | David Monniaux | 2020-10-31 | 1 | -3/+5 |
| * | reinstated old version | David Monniaux | 2020-10-30 | 1 | -58/+22 |
| * | reinstated previous forward_move function | David Monniaux | 2020-10-29 | 1 | -3/+28 |
| * | in CSE3 choose lowest variable as representative for moves | David Monniaux | 2020-10-29 | 1 | -12/+27 |
| * | new CSE3 | David Monniaux | 2020-10-27 | 1 | -21/+17 |
| * | some more tuning of CSE3 | David Monniaux | 2020-10-15 | 1 | -9/+18 |
| * | a bit of progress | David Monniaux | 2020-10-14 | 1 | -4/+7 |
| * | -fcse3-glb | David Monniaux | 2020-05-06 | 1 | -7/+17 |
| * | CSE3 across merges | David Monniaux | 2020-05-06 | 1 | -11/+25 |
| * | Adding copyrights | Cyril SIX | 2020-05-04 | 1 | -0/+12 |
| * | CSE3 across calls | David Monniaux | 2020-04-23 | 1 | -5/+17 |
| * | fix in CSE3 move propagation | David Monniaux | 2020-04-23 | 1 | -5/+14 |
| * | improvement in precision | David Monniaux | 2020-04-21 | 1 | -1/+3 |
| * | forward moves through CSE3 store | David Monniaux | 2020-04-21 | 1 | -2/+2 |
| * | CSE3: better builtin handling | David Monniaux | 2020-04-16 | 1 | -1/+24 |
| * | fix Icond now has a extra argument | David Monniaux | 2020-04-08 | 1 | -1/+1 |
| * | CSE3 alias analysis | David Monniaux | 2020-03-14 | 1 | -2/+23 |
| * | CSE3 analysis | David Monniaux | 2020-03-12 | 1 | -5/+5 |
| * | inductiveness test in CSE3 | David Monniaux | 2020-03-12 | 1 | -1/+23 |
| * | removed second analysis phase | David Monniaux | 2020-03-12 | 1 | -1/+3 |
| * | typing and store stuff | David Monniaux | 2020-03-12 | 1 | -9/+14 |
| * | store sound | David Monniaux | 2020-03-12 | 1 | -0/+5 |
| * | more lemmas | David Monniaux | 2020-03-12 | 1 | -6/+9 |
| * | lemmas on storev | David Monniaux | 2020-03-12 | 1 | -0/+27 |
| * | CSE3 ready to run? | David Monniaux | 2020-03-11 | 1 | -9/+9 |
| * | progress on CSE3 | David Monniaux | 2020-03-10 | 1 | -2/+3 |
| * | starts compiling but still fake | David Monniaux | 2020-03-10 | 1 | -5/+34 |
| * | CSE3: apply_instr' | David Monniaux | 2020-03-10 | 1 | -0/+30 |
| * | oper sound | David Monniaux | 2020-03-10 | 1 | -4/+3 |
| * | move sound | David Monniaux | 2020-03-10 | 1 | -0/+17 |
| * | moved no away | David Monniaux | 2020-03-10 | 1 | -8/+19 |
| * | oper2 | David Monniaux | 2020-03-10 | 1 | -1/+11 |
| * | rhs_find_op_sound | David Monniaux | 2020-03-10 | 1 | -0/+15 |
| * | eq_find_sound | David Monniaux | 2020-03-10 | 1 | -1/+36 |
| * | forward_move_l | David Monniaux | 2020-03-10 | 1 | -3/+9 |
| * | cse3: forward_move_sound | David Monniaux | 2020-03-09 | 1 | -2/+27 |
| * | get moves | David Monniaux | 2020-03-09 | 1 | -12/+3 |
| * | get_moves | David Monniaux | 2020-03-09 | 1 | -1/+33 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |