aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
...
* | | | Monday's work on RTLTunnelingproofPierre Goutagny2021-06-071-31/+153
* | | | Add RTLTunnelingproof.vPierre Goutagny2021-06-041-0/+170
* | | | Fix check_instr Icond target conditionsPierre Goutagny2021-06-041-2/+2
* | | | Write RTLTunneling.vPierre Goutagny2021-06-031-0/+125
* | | | Add RTLTunneling.vPierre Goutagny2021-06-031-0/+0
|/ / /
* | | Merge remote-tracking branch 'verimag/manuscript' into kvx-workCyril SIX2021-06-011-13/+11
|\ \ \
| * | | Do not rotate if the CB was already at the end.Cyril SIX2021-04-281-1/+5
| * | | Heuristic counter updateCyril SIX2021-04-281-12/+6
| |/ /
* | | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-014-545/+286
|\| |
| * | 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
* | | | [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
generated by cgit (git 2.34.1) at 2024-05-08 05:54:49 +0000