aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Changing to an opaq record in BTL info, this is a broken commitLéo Gourdin2021-05-201-0/+52
* Grouping common RTL functions, printer improvementLéo Gourdin2021-05-192-5/+2
* Merge remote-tracking branch 'origin/manuscript' into kvx-worksubmission_OOPSLA2021_AARCH64_KVXCyril SIX2021-04-133-511/+129
|\
| * CleaningCyril SIX2021-04-021-2/+1
| * More efficientCyril SIX2021-04-021-8/+12
| * Outermost loop detection worksCyril SIX2021-04-021-9/+10
| * Getting all loop bodiesCyril SIX2021-04-021-2/+36
| * get_loop_headers simplification (using the new get_loop_backedges)Cyril SIX2021-04-021-39/+7
| * Simple backedge detection (modified code from get_loop_headers)Cyril SIX2021-04-022-0/+43
| * Big simplification of get_loop_infoCyril SIX2021-03-311-111/+16
| * Simplification of the Linearize heuristic (same result functionally)Cyril SIX2021-03-301-216/+6
| * Simplifications on Linearize - details belowCyril SIX2021-03-291-205/+79
* | Adding more precise heuristic measuresCyril SIX2021-04-131-2/+62
* | Adding overpredictsCyril SIX2021-04-131-3/+6
* | Recording of prediction stats with COMPCERT_PROFILING_STATS environment flagCyril SIX2021-04-131-33/+93
* | removing unusued proof lineLéo Gourdin2021-04-091-1/+0
* | Important commit on expansions' mini CSE, and a draft for addptrofsLéo Gourdin2021-04-061-1/+2
* | add has_type infoDavid Monniaux2021-01-311-1/+3
|/
* Conditions now propagated by CSE3David Monniaux2021-01-205-264/+934
|\
| * totally switch off conditions in cse3David Monniaux2020-12-092-16/+21
| * begin implementing -fcse3-conditionsDavid Monniaux2020-12-092-8/+15
| * CSE3 + conditions proofDavid Monniaux2020-12-092-34/+58
| * apply_cond_soundDavid Monniaux2020-12-091-0/+14
| * apply_cond0_soundDavid Monniaux2020-12-091-1/+25
| * apply_cond1_soundDavid Monniaux2020-12-091-0/+30
| * proof for jumptableDavid Monniaux2020-12-091-1/+27
| * one 'admit' lessDavid Monniaux2020-12-091-2/+36
| * avancement dans les preuvesDavid Monniaux2020-12-091-1/+34
| * CSE3 compiles again, but some admitted lemmasDavid Monniaux2020-12-091-10/+8
| * progress moving to list of itemsDavid Monniaux2020-12-093-92/+233
| * analysis with Abst_sameDavid Monniaux2020-12-083-22/+39
| * CSE3 now runs on its own fixpoint iterator not based on Kildall.vDavid Monniaux2020-12-082-114/+3
| * Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-0813-80/+183
| |\
| * | start checking for bugsDavid Monniaux2020-12-021-2/+115
| * | attempt at initial analysisDavid Monniaux2020-12-021-1/+35
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-024-5/+487
| |\ \
| * | | not yet the transfer functions that record predicatesDavid Monniaux2020-11-263-9/+78
| * | | remains one admitDavid Monniaux2020-11-261-8/+46
| * | | is_condition_present_soundDavid Monniaux2020-11-263-5/+23
| * | | begin implementing cond tableDavid Monniaux2020-11-261-6/+13
| * | | ajouté Cond, tout passeDavid Monniaux2020-11-263-40/+168
| * | | passage à EquDavid Monniaux2020-11-263-189/+196
| * | | cond_valid_pointer_eqDavid Monniaux2020-11-251-0/+14
* | | | remove some useless "OK tt"Sylvain Boulmé2021-01-072-11/+11
* | | | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2021-01-074-92/+13
|\ \ \ \
| * | | | Making verify_mapping_mn_rec tail recursive (should fix arm CI) #231Cyril SIX2021-01-062-3/+2
| * | | | Solving a stack overflow issue (was failing in yarpgen ran000089 for armhf)Cyril SIX2021-01-061-9/+9
| * | | | Uniformizing a couple of debug print functionsCyril SIX2020-12-172-80/+2
* | | | | -fcse3-trivial-opsDavid Monniaux2021-01-072-3/+4
|/ / / /
* | | | Fixing wrong predictions on imbricated loopsCyril SIX2020-12-111-104/+114
generated by cgit (git 2.34.1) at 2024-06-02 16:40:22 +0000