Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | begin implementing -fcse3-conditions | David Monniaux | 2020-12-09 | 1 | -4/+8 |
| | |||||
* | apply_cond_sound | David Monniaux | 2020-12-09 | 1 | -0/+14 |
| | |||||
* | apply_cond0_sound | David Monniaux | 2020-12-09 | 1 | -1/+25 |
| | |||||
* | apply_cond1_sound | David Monniaux | 2020-12-09 | 1 | -0/+30 |
| | |||||
* | progress moving to list of items | David Monniaux | 2020-12-09 | 1 | -0/+2 |
| | |||||
* | analysis with Abst_same | David Monniaux | 2020-12-08 | 1 | -4/+10 |
| | |||||
* | is_condition_present_sound | David Monniaux | 2020-11-26 | 1 | -0/+16 |
| | |||||
* | ajouté Cond, tout passe | David Monniaux | 2020-11-26 | 1 | -24/+134 |
| | |||||
* | passage à Equ | David Monniaux | 2020-11-26 | 1 | -95/+100 |
| | |||||
* | store2_sound | David Monniaux | 2020-11-25 | 1 | -1/+1 |
| | |||||
* | clever_kill_store_sound | David Monniaux | 2020-11-25 | 1 | -7/+5 |
| | |||||
* | kill_store_sound | David Monniaux | 2020-11-25 | 1 | -0/+49 |
| | |||||
* | two lemmas admitted | David Monniaux | 2020-11-25 | 1 | -7/+91 |
| | |||||
* | refixcse3 | David Monniaux | 2020-11-03 | 1 | -18/+24 |
| | |||||
* | seems to work better | David Monniaux | 2020-10-31 | 1 | -0/+32 |
| | |||||
* | reinstated old version | David Monniaux | 2020-10-30 | 1 | -154/+12 |
| | |||||
* | reinstated previous forward_move function | David Monniaux | 2020-10-29 | 1 | -8/+70 |
| | |||||
* | in CSE3 choose lowest variable as representative for moves | David Monniaux | 2020-10-29 | 1 | -31/+76 |
| | |||||
* | new CSE3 | David Monniaux | 2020-10-27 | 1 | -9/+44 |
| | |||||
* | some more tuning of CSE3 | David Monniaux | 2020-10-15 | 1 | -1/+5 |
| | |||||
* | a bit of progress | David Monniaux | 2020-10-14 | 1 | -0/+23 |
| | |||||
* | -fcse3-glb | David Monniaux | 2020-05-06 | 1 | -7/+11 |
| | |||||
* | Adding copyrights | Cyril SIX | 2020-05-04 | 1 | -0/+11 |
| | |||||
* | CSE3 across calls | David Monniaux | 2020-04-23 | 1 | -5/+16 |
| | |||||
* | fix in CSE3 move propagation | David Monniaux | 2020-04-23 | 1 | -8/+18 |
| | |||||
* | improvement in precision | David Monniaux | 2020-04-21 | 1 | -5/+31 |
| | |||||
* | forward moves through CSE3 store | David Monniaux | 2020-04-21 | 1 | -4/+4 |
| | |||||
* | CSE3: better builtin handling | David Monniaux | 2020-04-16 | 1 | -0/+30 |
| | |||||
* | CSE3 alias analysis | David Monniaux | 2020-03-14 | 1 | -1/+38 |
| | |||||
* | progress in proofs | David Monniaux | 2020-03-13 | 1 | -17/+8 |
| | |||||
* | moving forward in proofs | David Monniaux | 2020-03-13 | 1 | -1/+80 |
| | |||||
* | some automation | David Monniaux | 2020-03-13 | 1 | -0/+31 |
| | |||||
* | fmap_sem | David Monniaux | 2020-03-13 | 1 | -3/+3 |
| | |||||
* | begin writing match states predicates | David Monniaux | 2020-03-12 | 1 | -0/+2 |
| | |||||
* | CSE3 analysis | David Monniaux | 2020-03-12 | 1 | -0/+75 |
| | |||||
* | store sound | David Monniaux | 2020-03-12 | 1 | -1/+19 |
| | |||||
* | more lemmas | David Monniaux | 2020-03-12 | 1 | -2/+36 |
| | |||||
* | lemmas on storev | David Monniaux | 2020-03-12 | 1 | -0/+34 |
| | |||||
* | starts compiling but still fake | David Monniaux | 2020-03-10 | 1 | -6/+6 |
| | |||||
* | oper sound | David Monniaux | 2020-03-10 | 1 | -3/+27 |
| | |||||
* | move sound | David Monniaux | 2020-03-10 | 1 | -1/+33 |
| | |||||
* | oper1 | David Monniaux | 2020-03-10 | 1 | -0/+14 |
| | |||||
* | moved no away | David Monniaux | 2020-03-10 | 1 | -4/+4 |
| | |||||
* | oper2 | David Monniaux | 2020-03-10 | 1 | -1/+120 |
| | |||||
* | forward_move_rhs_sound | David Monniaux | 2020-03-10 | 1 | -0/+12 |
| | |||||
* | rhs_find_op_sound | David Monniaux | 2020-03-10 | 1 | -10/+42 |
| | |||||
* | eq_find_sound | David Monniaux | 2020-03-10 | 1 | -0/+16 |
| | |||||
* | forward_move_l | David Monniaux | 2020-03-10 | 1 | -0/+20 |
| | |||||
* | kill_mem_sound | David Monniaux | 2020-03-09 | 1 | -6/+52 |
| | |||||
* | cse3: forward_move_sound | David Monniaux | 2020-03-09 | 1 | -1/+45 |
| |