aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| | * | clightgen -short-idents : do not use $"xxx" notation everXavier Leroy2020-06-011-1/+1
| | * | Add a canonical encoding of identifiers as numbers and use it in clightgen (#...Xavier Leroy2020-05-194-20/+204
| | * | Move Commandline to the lib/ directoryXavier Leroy2020-05-052-0/+0
| | * | Update the list of dual-licensed filesXavier Leroy2020-05-051-2/+2
| | * | Dual-license aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v}Xavier Leroy2020-05-053-0/+9
| | * | Import ListNotations explicitlyXavier Leroy2020-05-041-0/+1
| | * | Revert "Do not use the list notation `[]`"Xavier Leroy2020-05-041-8/+8
| | * | Do not use the list notation `[]`Xavier Leroy2020-05-041-8/+8
| | * | Do not use "Declare Scope", introduced in Coq 8.10 onlyXavier Leroy2020-05-041-1/+0
| | * | Coq-MenhirLib: explicit import ListNotations (#354)Jacques-Henri Jourdan2020-05-047-4/+12
| | * | Install "compcert.config" file along the Coq developmentXavier Leroy2020-04-292-1/+19
| | * | Updated .gitignoreBernhard Schommer2020-04-271-0/+1
| | * | Simplify the generation of driver/Version.mlBernhard Schommer2020-04-271-3/+8
| | * | Move reserved_registers to CPragmas.Bernhard Schommer2020-04-204-8/+8
| | * | Support for coq 8.11.1.Bernhard Schommer2020-04-201-2/+2
| | * | Check for errors after each pass.Bernhard Schommer2020-04-201-1/+8
| | * | Added warning for packed composite with bitfields.Bernhard Schommer2020-04-201-0/+2
| | * | Add location to transform functions.Bernhard Schommer2020-04-204-28/+28
* | | | start checking for bugsDavid Monniaux2020-12-022-3/+116
* | | | attempt at initial analysisDavid Monniaux2020-12-021-1/+35
* | | | cond_depends_onDavid Monniaux2020-12-023-21/+21
* | | | simpl -> cbnDavid Monniaux2020-12-021-9/+9
* | | | cond_depends_on_memory for KVXDavid Monniaux2020-12-021-4/+17
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-0279-731/+10580
|\ \ \ \ | | |_|/ | |/| |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassCyril SIX2020-12-016-11/+161
| |\ \ \
| * | | | Ignore loopback edges on tail-duplicateCyril SIX2020-12-011-0/+2
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-2413-31/+343
| |\ \ \ \
| * | | | | prepass scheduling proof finished !Sylvain Boulmé2020-11-201-24/+56
| * | | | | merge nouveau tunnelingDavid Monniaux2020-11-191-1/+1
| * | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-198-270/+728
| |\ \ \ \ \
| * | | | | | seval_builtin_sval_preservedDavid Monniaux2020-11-171-1/+4
| * | | | | | a little lemma on list of builtinsDavid Monniaux2020-11-171-2/+15
| * | | | | | there remains two tricky casesDavid Monniaux2020-11-161-3/+14
| * | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-062-27/+32
| |\ \ \ \ \ \ | | | |_|_|/ / | | |/| | | |
| * | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-055-31/+114
| |\ \ \ \ \ \
| * | | | | | | disable debug printing in schedulerDavid Monniaux2020-11-042-7/+9
| * | | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-041-1/+2
| |\ \ \ \ \ \ \
| * \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-037-36/+121
| |\ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-315-17/+121
| |\ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-304-168/+78
| |\ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-295-48/+109
| |\ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-284-42/+27
| |\ \ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-277-63/+166
| |\ \ \ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-277-10/+277
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | | | | improved CSE3David Monniaux2020-10-271-12/+12
| * | | | | | | | | | | | | | | progress in proofs on new CSE3David Monniaux2020-10-271-3/+34
| * | | | | | | | | | | | | | | deactivate LICM by defaultDavid Monniaux2020-10-272-21/+12
| * | | | | | | | | | | | | | | begin fixing CSE3 to keep more inductive stuffDavid Monniaux2020-10-272-10/+19
| * | | | | | | | | | | | | | | invariant printing more aligned with RTL dumpsDavid Monniaux2020-10-271-2/+2
| * | | | | | | | | | | | | | | print invariantsDavid Monniaux2020-10-271-11/+46
generated by cgit (git 2.34.1) at 2024-07-12 03:06:23 +0000