aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* 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
| |\ \ \
| | * | | Added option -ftracelinearize which linearizes based on ifnot branchesCyril SIX2020-02-122-4/+55
| * | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-061-3/+3
| |\| | |
| | * | | accessors for records are now not extracted it seemsDavid Monniaux2020-02-061-3/+3
| * | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-063-18/+593
| |\| | |
| | * | | Added flag to desactivate condition inversionCyril SIX2020-02-031-1/+2
| | * | | Adding threshold to duplicate instructionsCyril SIX2020-01-311-6/+12
| | * | | Added debug message when inverting ifso ifnotCyril SIX2020-01-241-1/+3
| | * | | Oracle inverting branches when trace does not go in fallthruCyril SIX2020-01-241-2/+21
| | * | | Revert "Modified the hook for the oracle"Cyril SIX2020-01-233-12/+8
| | * | | Verificator finished for handling reversed IcondCyril SIX2020-01-232-11/+18
| | * | | Added clause in match_inst to allow Icond reversalCyril SIX2020-01-231-4/+13
| | * | | Modified the hook for the oracleCyril SIX2020-01-233-8/+12
| | * | | Fixing bug caused by get_predecessors returning duplicatesCyril SIX2020-01-231-5/+8
| | * | | Printing traces right before duplicatingCyril SIX2020-01-231-5/+2
| | * | | Fixing bug (used physical instead of structural inequality)Cyril SIX2020-01-221-1/+2
| | * | | Merge branch 'mppa-work' into mppa-duplicate-oracleCyril SIX2020-01-222-0/+1134
| | |\ \ \
| | * | | | Fixing is_empty functionCyril SIX2020-01-221-3/+3
| | * | | | Branch duplication implementationCyril SIX2020-01-221-12/+94
| | * | | | Set up the groundbase for doing the duplicationCyril SIX2020-01-171-4/+14
| | * | | | Removed unnecessary .mli file (provoked compilation problems)Cyril SIX2020-01-171-12/+0
| | * | | | Adding more debug elementsCyril SIX2020-01-151-1/+9
| | * | | | Typo in printfCyril SIX2020-01-131-1/+1
| | * | | | Opcode heuristic done for K1cCyril SIX2019-12-162-1/+3
| | * | | | Stub for opcode heuristicCyril SIX2019-12-162-4/+12
| | * | | | Fixing loop heuristic for the way CompCert handles loopsCyril SIX2019-12-111-11/+19
| | * | | | Implemented call, return, store and loop heuristicsCyril SIX2019-12-111-2/+55
| | * | | | Function to look ahead unconditionallyCyril SIX2019-12-111-0/+12
| | * | | | Loop headers detection works!Cyril SIX2019-12-111-3/+17
| | * | | | Dominators approach not working well ==> opting for visit approachCyril SIX2019-12-101-23/+73
| | * | | | Calcul de dominateurs a l'air de marcherCyril SIX2019-12-101-88/+144