aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * | | | | disable printing debug infoDavid Monniaux2021-07-191-1/+1
| * | | | | debugprint flag not to trueDavid Monniaux2021-07-191-7/+0
| | |_|_|/ | |/| | |
| * | | | move back to "list" scheduler since regpres is buggyDavid Monniaux2021-07-191-1/+1
| * | | | Make prepass scheduling sensitive to register pressure, by Nicolas Nardino.David Monniaux2021-07-1629-36/+2146
| | |_|/ | |/| |
| * | | adding mayundef resource_bounds (not changing perfs)Léo Gourdin2021-06-251-1/+2
| * | | Replacing default notrap load value by Vundef everywherecsix-PhDCyril SIX2021-06-1821-49/+39
| | |/ | |/|
| * | fix modeling issue (Vundef for load outside of bounds)David Monniaux2021-06-161-2/+7
| * | Use qemu-6.0.0 for PPC as the 3.1.0 version shipping with the Debian in the d...David Monniaux2021-06-121-2/+5
| * | show qemu versionDavid Monniaux2021-06-111-0/+1
| * | disable ppc partiallyDavid Monniaux2021-06-111-2/+6
| * | compile non yarpgen tests without -static; this should workDavid Monniaux2021-06-111-4/+4
| * | disable PPC64; can't link and don't know whyDavid Monniaux2021-06-111-2/+2
| * | fix bad pathsDavid Monniaux2021-06-111-2/+2
| * | don't use -static on ppcDavid Monniaux2021-06-111-4/+4
| * | path issuesDavid Monniaux2021-06-111-6/+6
| * | add PPC to CI and remove ugly hack for qemu linker pathsDavid Monniaux2021-06-111-56/+62
| * | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2021-06-111-39/+0
| |\ \
| | * | remove filter fileLéo Gourdin2021-06-101-39/+0
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into kvx-workDavid Monniaux2021-06-112-3/+13
| |\ \ \ | | |/ / | |/| |
| | * | x86 assembly: fix the comment delimiter for macos and make it per-OSXavier Leroy2021-06-101-3/+11
| * | | push afadl test exampleLéo Gourdin2021-06-092-0/+21
| * | | Merge branch 'kvx-work' of https://gricad-gitlab.univ-grenoble-alpes.fr/sixcy...Olivier Lebeltel2021-06-091-1/+1
| |\ \ \
| | * | | comment is now ## due to some weird MacOS bugDavid Monniaux2021-06-091-1/+1
| * | | | added config_macos_x86_64.shOlivier Lebeltel2021-06-091-0/+1
| |/ / /
| * | | MacOS compatibilityDavid Monniaux2021-06-091-1/+1
| * | | run CI on kvx-work-ssa kvx-work-velusDavid Monniaux2021-06-081-49/+57
| * | | omega -> liaDavid Monniaux2021-06-081-8/+8
| * | | coq 8.13.2David Monniaux2021-06-071-2/+1
| * | | divisionDavid Monniaux2021-06-072-3/+4
| * | | timingDavid Monniaux2021-06-072-0/+117
| * | | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2021-06-06340-6016/+11801
| |\ \ \ | | | |/ | | |/|
| * | | omega -> liaDavid Monniaux2021-06-062-26/+28
* | | | Change "Tunneling" to "LTLTunneling" everywherePierre Goutagny2021-06-1710-14/+14
* | | | 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
* | | | Move rtl_tunneling to a more interesting placePierre Goutagny2021-06-151-1/+1
* | | | Factorise RTL Tunneling pass in compiler_expandPierre Goutagny2021-06-151-1/+3
* | | | Add RTL Tunneling as a passPierre Goutagny2021-06-143-1/+8
* | | | 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
* | | | Monday's work on RTLTunnelingproofPierre Goutagny2021-06-071-31/+153
* | | | Add RTLTunnelingproof.vPierre Goutagny2021-06-042-1/+171
* | | | Fix check_instr Icond target conditionsPierre Goutagny2021-06-041-2/+2
* | | | Write RTLTunneling.vPierre Goutagny2021-06-031-0/+125
* | | | Add RTLTunneling.vPierre Goutagny2021-06-032-0/+1
| |/ / |/| |
* | | Remove install path bricolage for kvxv3.9_kvxCyril SIX2021-06-012-4/+5
generated by cgit (git 2.34.1) at 2024-06-30 11:20:24 +0000