Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | invariant guaranteed | David Monniaux | 2020-02-04 | 2 | -4/+56 |
* | wellformedness for memory | David Monniaux | 2020-02-04 | 2 | -17/+158 |
* | begin well formedness | David Monniaux | 2020-02-04 | 2 | -15/+130 |
* | gremove_t | David Monniaux | 2020-02-04 | 1 | -0/+36 |
* | gcombine_null | David Monniaux | 2020-02-04 | 1 | -0/+13 |
* | gcombine_null | David Monniaux | 2020-02-04 | 1 | -1/+39 |
* | stuff information into a record | David Monniaux | 2020-02-04 | 2 | -46/+63 |
* | another version of proof that allows Vundef in loaded values | David Monniaux | 2020-02-03 | 1 | -18/+18 |
* | comments | David Monniaux | 2020-02-03 | 2 | -0/+14 |
* | forgot a "in *" | David Monniaux | 2020-01-28 | 1 | -20/+1 |
* | with loads too ? | David Monniaux | 2020-01-28 | 2 | -8/+119 |
* | load_sound | David Monniaux | 2020-01-28 | 1 | -0/+96 |
* | find_load_sound | David Monniaux | 2020-01-28 | 1 | -4/+92 |
* | begin adding loads | David Monniaux | 2020-01-28 | 1 | -2/+7 |
* | much better - seems to eliminate CSE not containing loads | David Monniaux | 2020-01-28 | 2 | -2/+18 |
* | still buggy | David Monniaux | 2020-01-28 | 2 | -56/+95 |
* | connected (just a silly problem) | David Monniaux | 2020-01-28 | 6 | -8/+51 |
* | CSE2 now works for expressions | David Monniaux | 2020-01-28 | 2 | -47/+69 |
* | now going back to op | David Monniaux | 2020-01-28 | 1 | -45/+6 |
* | rework | David Monniaux | 2020-01-28 | 1 | -20/+49 |
* | sem_rel_b_ge | David Monniaux | 2020-01-28 | 1 | -61/+152 |
* | sem_rel_b_ge | David Monniaux | 2020-01-28 | 1 | -18/+77 |
* | CSE2 split in two files | David Monniaux | 2020-01-28 | 3 | -827/+838 |
* | progress | David Monniaux | 2020-01-27 | 1 | -0/+467 |
* | use in transformation | David Monniaux | 2020-01-27 | 1 | -3/+21 |
* | find_op_sound | David Monniaux | 2020-01-27 | 1 | -1/+110 |
* | goes to the end but does not find available ops | David Monniaux | 2020-01-27 | 1 | -13/+5 |
* | simpler definitions | David Monniaux | 2020-01-27 | 1 | -41/+24 |
* | static analysis done | David Monniaux | 2020-01-27 | 1 | -20/+7 |
* | kill_mem_sound | David Monniaux | 2020-01-27 | 1 | -8/+59 |
* | renamed kill_reg into kill_mem | David Monniaux | 2020-01-27 | 1 | -11/+11 |
* | gen_oper_sound | David Monniaux | 2020-01-27 | 1 | -1/+37 |
* | oper_sound | David Monniaux | 2020-01-27 | 1 | -0/+27 |
* | oper1_sound | David Monniaux | 2020-01-27 | 1 | -1/+10 |
* | arg replace | David Monniaux | 2020-01-27 | 1 | -1/+87 |
* | move sound | David Monniaux | 2020-01-27 | 1 | -19/+85 |
* | begin proving stuff | David Monniaux | 2020-01-27 | 1 | -0/+436 |
* | Remove __builtin_nop from list of x86 builtins. | Bernhard Schommer | 2020-01-03 | 1 | -3/+0 |
* | Revert "Remove `__builtin_nop` for some architectures. (#208)" | Bernhard Schommer | 2020-01-03 | 14 | -3/+33 |
* | Added error for unknown builtin functions. (#208) | Bernhard Schommer | 2019-12-21 | 1 | -1/+6 |
* | Remove `__builtin_nop` for some architectures. (#208) | Bernhard Schommer | 2019-12-21 | 14 | -33/+3 |
* | The SP register has dwarf register number 31. | Bernhard Schommer | 2019-12-11 | 1 | -1/+1 |
* | Allow Coq 8.10.2. | Bernhard Schommer | 2019-12-03 | 1 | -1/+1 |
* | Fix for AArch64 alignment problem (#206) | Bernhard Schommer | 2019-11-28 | 4 | -2/+13 |
* | Added dwarf register numbers for aarch64 | Bernhard Schommer | 2019-11-28 | 1 | -3/+18 |
* | Added back unused_ais_parameter warning. | Bernhard Schommer | 2019-11-26 | 1 | -0/+1 |
* | Simplified diagnostics module. | Bernhard Schommer | 2019-11-25 | 1 | -118/+41 |
* | Remove no longer needed file PrintLTLin | Bernhard Schommer | 2019-11-12 | 1 | -115/+0 |
* | Use `intuition idtac` instead of `intuition` (#321) | Vincent Laporte | 2019-11-12 | 1 | -1/+1 |
* | Raise minimal required versions for OCaml and Coq (#203) | Bernhard Schommer | 2019-10-31 | 1 | -9/+4 |