aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-014-10/+18
* replacing omega with lia in some fileLéo Gourdin2021-03-293-7/+8
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-2335-708/+737
|\
| * Fix regression on PowerPC / DiabXavier Leroy2021-02-231-2/+7
| * Section handling: finer control of variable initializationXavier Leroy2021-02-233-10/+25
| * Introduce and use PrintAsmaux.variable_sectionXavier Leroy2021-02-231-7/+12
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-2110-60/+60
| * Improve branch tunnelingXavier Leroy2021-01-132-60/+328
| * Revised correctness proof for record_gotoXavier Leroy2021-01-131-68/+29
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-2927-636/+636
| * Changed cc_varargs to an option typeBernhard Schommer2020-12-251-1/+1
* | 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
* | | | | Fixing exponential blowup on get_loop_info.mark_path.exploreCyril SIX2020-12-091-33/+44
* | | | | Flushing debug outputCyril SIX2020-12-091-1/+1
* | | | | The last fix for get_loop_info was giving false positives. Fixing that.Cyril SIX2020-12-081-2/+12
* | | | | Fixing get_loop_info : part 2Cyril SIX2020-12-081-8/+28
* | | | | Fixing loop detection in get_loop_info - part 1Cyril SIX2020-12-081-16/+8
* | | | | Moving codeCyril SIX2020-12-081-71/+72
generated by cgit (git 2.34.1) at 2024-06-02 15:45:48 +0000