Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | CSE3 analysis proof | David Monniaux | 2020-03-07 | 1 | -0/+35 |
* | get_kills_has_arg | David Monniaux | 2020-03-07 | 1 | -0/+21 |
* | get_kills_has_lhs | David Monniaux | 2020-03-06 | 1 | -7/+25 |
* | xlkills | David Monniaux | 2020-03-06 | 1 | -1/+21 |
* | xlkills | David Monniaux | 2020-03-06 | 1 | -10/+54 |
* | xget_kills_monotone | David Monniaux | 2020-03-05 | 1 | -4/+27 |
* | xget_kills | David Monniaux | 2020-03-05 | 1 | -0/+74 |
* | just the analysis | David Monniaux | 2020-03-05 | 1 | -0/+3 |
* | more about extraction and linking | David Monniaux | 2020-03-05 | 1 | -0/+2 |
* | streamlined lattice code | David Monniaux | 2020-03-05 | 1 | -114/+1 |
* | begin CSE3 | David Monniaux | 2020-03-05 | 1 | -0/+76 |
* | fixed CSE2 for mppa_k1c | David Monniaux | 2020-03-03 | 5 | -784/+213 |
|\ | |||||
| * | CSE2 alias analysis for Risc-V | David Monniaux | 2020-03-03 | 3 | -30/+2 |
| * | moved away x86-dependent parts | David Monniaux | 2020-03-03 | 1 | -38/+0 |
| * | modularize proof | David Monniaux | 2020-03-03 | 1 | -29/+10 |
| * | may_overlap_sound | David Monniaux | 2020-03-03 | 1 | -0/+38 |
| * | starting to move x86 stuff to x86 | David Monniaux | 2020-03-03 | 1 | -201/+1 |
| * | offsets in globals for x86 | David Monniaux | 2020-03-03 | 2 | -2/+82 |
| * | globals alias analysis for x86 | David Monniaux | 2020-03-03 | 2 | -10/+59 |
| * | with indexed/indexed alias analysis for x86 | David Monniaux | 2020-03-03 | 2 | -4/+26 |
| * | kill_store_sound | David Monniaux | 2020-03-02 | 1 | -10/+25 |
| * | kill_store1_sound | David Monniaux | 2020-03-02 | 1 | -3/+41 |
| * | load_store_away | David Monniaux | 2020-03-02 | 1 | -1/+2 |
| * | swap predicate | David Monniaux | 2020-03-02 | 2 | -13/+27 |
| * | works on x86 x86_64 | David Monniaux | 2020-03-02 | 1 | -29/+47 |
| * | playing with offsets | David Monniaux | 2020-03-02 | 1 | -1/+67 |
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2-naive | David Monniaux | 2020-03-02 | 17 | -96/+174 |
| |\ | |||||
| | * | Weaker ec_readonly condition over external calls (#225) | Xavier Leroy | 2020-03-02 | 1 | -3/+2 |
| | * | Define IRC.class_of_type for types Tany32, Tany64 | Xavier Leroy | 2020-03-02 | 1 | -1/+2 |
* | | | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe... | David Monniaux | 2020-03-03 | 68 | -342/+4246 |
|\ \ \ | |||||
| * \ \ | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-02-14 | 2 | -4/+55 |
| |\ \ \ | |||||
| | * | | | Added option -ftracelinearize which linearizes based on ifnot branches | Cyril SIX | 2020-02-12 | 2 | -4/+55 |
| * | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-02-06 | 1 | -3/+3 |
| |\| | | | |||||
| | * | | | accessors for records are now not extracted it seems | David Monniaux | 2020-02-06 | 1 | -3/+3 |
| * | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-02-06 | 3 | -18/+593 |
| |\| | | | |||||
| | * | | | Added flag to desactivate condition inversion | Cyril SIX | 2020-02-03 | 1 | -1/+2 |
| | * | | | Adding threshold to duplicate instructions | Cyril SIX | 2020-01-31 | 1 | -6/+12 |
| | * | | | Added debug message when inverting ifso ifnot | Cyril SIX | 2020-01-24 | 1 | -1/+3 |
| | * | | | Oracle inverting branches when trace does not go in fallthru | Cyril SIX | 2020-01-24 | 1 | -2/+21 |
| | * | | | Revert "Modified the hook for the oracle" | Cyril SIX | 2020-01-23 | 3 | -12/+8 |
| | * | | | Verificator finished for handling reversed Icond | Cyril SIX | 2020-01-23 | 2 | -11/+18 |
| | * | | | Added clause in match_inst to allow Icond reversal | Cyril SIX | 2020-01-23 | 1 | -4/+13 |
| | * | | | Modified the hook for the oracle | Cyril SIX | 2020-01-23 | 3 | -8/+12 |
| | * | | | Fixing bug caused by get_predecessors returning duplicates | Cyril SIX | 2020-01-23 | 1 | -5/+8 |
| | * | | | Printing traces right before duplicating | Cyril SIX | 2020-01-23 | 1 | -5/+2 |
| | * | | | Fixing bug (used physical instead of structural inequality) | Cyril SIX | 2020-01-22 | 1 | -1/+2 |
| | * | | | Merge branch 'mppa-work' into mppa-duplicate-oracle | Cyril SIX | 2020-01-22 | 2 | -0/+1134 |
| | |\ \ \ | |||||
| | * | | | | Fixing is_empty function | Cyril SIX | 2020-01-22 | 1 | -3/+3 |
| | * | | | | Branch duplication implementation | Cyril SIX | 2020-01-22 | 1 | -12/+94 |
| | * | | | | Set up the groundbase for doing the duplication | Cyril SIX | 2020-01-17 | 1 | -4/+14 |