aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Merge ../kvx-work into kvx_fp_divisionDavid Monniaux2022-02-031-2/+2
|\
| * Merge remote-tracking branch 'absint/master' into merge_absintDavid Monniaux2022-02-021-2/+2
| |\
| | * Enforce evaluation order in IRC.add_interf and IRC.add_prefXavier Leroy2021-12-071-2/+2
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx_fp_divisionDavid Monniaux2021-12-142-3/+3
|\| |
| * | Merge remote-tracking branch 'absint/master' into towards_3.10David Monniaux2021-12-012-3/+3
| |\|
| | * An improved PTree data structure (#420)Xavier Leroy2021-11-162-3/+3
* | | some more fixed etc. constructsDavid Monniaux2021-12-121-0/+156
|/ /
* | Merge branch 'RTL_has_loaded' into kvx-workLéo Gourdin2021-11-0223-1382/+1324
|\ \
| * | bugfixLéo Gourdin2021-11-021-2/+2
| * | being more archi-independantLéo Gourdin2021-11-028-22/+19
| * | Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-0223-1377/+1322
* | | Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-292-2/+2
|\ \ \ | |/ / |/| / | |/
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-032-2/+2
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-242-5/+8
|\|
| * Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-151-2/+5
| * Handle the new warnings of OCaml 4.13Xavier Leroy2021-09-131-3/+3
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-082-8/+10
| * Emit no entry for variables without init in json.Bernhard Schommer2021-04-291-1/+7
| * Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-191-1/+1
* | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2021-09-013-5/+107
|\ \
| * | cleanupLéo Gourdin2021-09-011-9/+0
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-workLéo Gourdin2021-09-015-89/+24
| |\ \
| * \ \ [MERGE] BTL into kvx-work (replacing RTLpath)Léo Gourdin2021-09-013-5/+116
| |\ \ \
| | * \ \ Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-1038-738/+774
| | |\ \ \
| | * | | | [disabled checker] BTL Scheduling and Renumbering OK!Léo Gourdin2021-05-271-0/+1
| | * | | | Moving common tools, adding liveness input/output information to BTL generati...Léo Gourdin2021-05-243-2/+39
| | * | | | 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/parameterized-cse3' into kvx-workDavid Monniaux2021-09-014-61/+79
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | |
| * | | | | more parameterizationDavid Monniaux2021-07-161-2/+0
| * | | | | make operations cse3 parametricDavid Monniaux2021-07-162-6/+10
| * | | | | make trivial ops parametricDavid Monniaux2021-07-162-6/+7
| * | | | | make conditions a parameter in CSE3David Monniaux2021-07-162-3/+12
| * | | | | rename parameterized versionsDavid Monniaux2021-07-162-38/+38
| * | | | | make CSE3 condition parametricDavid Monniaux2021-07-162-29/+42
| * | | | | rm condition parametrization in CSE3analysisDavid Monniaux2021-07-162-13/+6
* | | | | | RTLTunneling: fix comments and authors informationSylvain Boulmé2021-08-245-89/+24
| |/ / / / |/| | | |
* | | | | remove default_notrap_load_valueSylvain Boulmé2021-07-241-1/+1
* | | | | Merge branch 'kvx-work' into rtl-tunnelingSylvain Boulmé2021-07-2413-25/+18
|\| | | |
| * | | | Replacing default notrap load value by Vundef everywherecsix-PhDCyril SIX2021-06-1813-25/+18
| | |/ / | |/| |
* | | | Change "Tunneling" to "LTLTunneling" everywherePierre Goutagny2021-06-175-5/+5
* | | | Use Tunnelinglibs in TunnelingauxPierre Goutagny2021-06-171-256/+81
* | | | Simplify tunneling factorisationPierre Goutagny2021-06-172-168/+173
* | | | Use Tunnelinglibs in RTLTunnelingauxPierre Goutagny2021-06-162-265/+123
* | | | Add Tunneling factorisation modulePierre Goutagny2021-06-161-0/+237
* | | | Add RTL Tunneling as a passPierre Goutagny2021-06-142-0/+6
* | | | Add the RTLTunneling oraclePierre Goutagny2021-06-141-0/+284
* | | | Complete RTLTunnelingproofPierre Goutagny2021-06-111-16/+66
* | | | Complete `tunnel_step_correct` proof up to IjumptablePierre Goutagny2021-06-101-9/+227
* | | | Starts proof for `tunnel_step_correct`Pierre Goutagny2021-06-091-15/+120
generated by cgit (git 2.34.1) at 2024-04-27 06:16:05 +0000