aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* printing created hashesDavid Monniaux2020-03-101-2/+54
* starts compiling but still fakeDavid Monniaux2020-03-105-11/+241
* CSE3: apply_instr'David Monniaux2020-03-101-0/+30
* oper soundDavid Monniaux2020-03-102-7/+30
* move soundDavid Monniaux2020-03-102-1/+50
* oper1David Monniaux2020-03-101-0/+14
* moved no awayDavid Monniaux2020-03-102-12/+23
* oper2David Monniaux2020-03-102-2/+131
* forward_move_rhs_soundDavid Monniaux2020-03-101-0/+12
* rhs_find_op_soundDavid Monniaux2020-03-102-10/+57
* eq_find_soundDavid Monniaux2020-03-102-1/+52
* forward_move_lDavid Monniaux2020-03-102-3/+29
* kill_mem_soundDavid Monniaux2020-03-091-6/+52
* cse3: forward_move_soundDavid Monniaux2020-03-092-3/+72
* get movesDavid Monniaux2020-03-092-30/+4
* CSE3David Monniaux2020-03-091-0/+21
* get_movesDavid Monniaux2020-03-091-1/+33
* kill_reg_soundDavid Monniaux2020-03-092-3/+88
* moved stuff aroundDavid Monniaux2020-03-092-177/+155
* CSE3 analysis proofDavid Monniaux2020-03-071-0/+35
* get_kills_has_argDavid Monniaux2020-03-071-0/+21
* get_kills_has_lhsDavid Monniaux2020-03-061-7/+25
* xlkillsDavid Monniaux2020-03-061-1/+21
* xlkillsDavid Monniaux2020-03-061-10/+54
* xget_kills_monotoneDavid Monniaux2020-03-051-4/+27
* xget_killsDavid Monniaux2020-03-051-0/+74
* just the analysisDavid Monniaux2020-03-051-0/+3
* more about extraction and linkingDavid Monniaux2020-03-051-0/+2
* streamlined lattice codeDavid Monniaux2020-03-051-114/+1
* begin CSE3David Monniaux2020-03-051-0/+76
* fixed CSE2 for mppa_k1cDavid Monniaux2020-03-035-784/+213
|\
| * CSE2 alias analysis for Risc-VDavid Monniaux2020-03-033-30/+2
| * moved away x86-dependent partsDavid Monniaux2020-03-031-38/+0
| * modularize proofDavid Monniaux2020-03-031-29/+10
| * may_overlap_soundDavid Monniaux2020-03-031-0/+38
| * starting to move x86 stuff to x86David Monniaux2020-03-031-201/+1
| * offsets in globals for x86David Monniaux2020-03-032-2/+82
| * globals alias analysis for x86David Monniaux2020-03-032-10/+59
| * with indexed/indexed alias analysis for x86David Monniaux2020-03-032-4/+26
| * kill_store_soundDavid Monniaux2020-03-021-10/+25
| * kill_store1_soundDavid Monniaux2020-03-021-3/+41
| * load_store_awayDavid Monniaux2020-03-021-1/+2
| * swap predicateDavid Monniaux2020-03-022-13/+27
| * works on x86 x86_64David Monniaux2020-03-021-29/+47
| * playing with offsetsDavid Monniaux2020-03-021-1/+67
| * Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2-naiveDavid Monniaux2020-03-0217-96/+174
| |\
| | * Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-021-3/+2
| | * Define IRC.class_of_type for types Tany32, Tany64Xavier Leroy2020-03-021-1/+2
* | | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-0368-342/+4246
|\ \ \
| * \ \ Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-142-4/+55
| |\ \ \
generated by cgit (git 2.34.1) at 2024-06-03 00:55:59 +0000