| Commit message (Expand) | Author | Age | Files | Lines | ||
|---|---|---|---|---|---|---|
| ... | ||||||
| | | * | | Use library function. | Bernhard Schommer | 2020-06-28 | 1 | -4/+1 | |
| | | * | | Use Hashtbl.find_opt. | Bernhard Schommer | 2020-06-28 | 8 | -9/+8 | |
| | | * | | Eliminate known builtins whose result is ignored | Xavier Leroy | 2020-06-25 | 2 | -40/+54 | |
| | | * | | Improve printing of builtin function invocations | Xavier Leroy | 2020-06-25 | 1 | -0/+3 | |
| | | * | | Preliminary support for Coq 8.12 | Xavier Leroy | 2020-06-21 | 2 | -4/+4 | |
| | | * | | Transform non-recursive Fixpoint into Definition | Xavier Leroy | 2020-06-21 | 3 | -3/+3 | |
| | | * | | SimplExpr: remove unused definition "sd_cast_set" | Xavier Leroy | 2020-06-15 | 1 | -2/+0 | |
| | | * | | SimplExpr: better translation of casts in a "for effects" context | Xavier Leroy | 2020-06-15 | 3 | -136/+166 | |
| | | * | | Compatibility with coq 8.11.2 | Bernhard Schommer | 2020-06-08 | 1 | -1/+1 | |
| | | * | | Improve portability of the test for annotations inclightgen | Xavier Leroy | 2020-06-05 | 2 | -0/+4 | |
| | | * | | clightgen: fix the printing of annotations | Xavier Leroy | 2020-06-05 | 2 | -59/+14 | |
| | | * | | clightgen: fix usage message | Xavier Leroy | 2020-06-01 | 1 | -2/+2 | |
| | | * | | clightgen -short-idents : do not use $"xxx" notation ever | Xavier Leroy | 2020-06-01 | 1 | -1/+1 | |
| | | * | | Add a canonical encoding of identifiers as numbers and use it in clightgen (#... | Xavier Leroy | 2020-05-19 | 4 | -20/+204 | |
| | | * | | Move Commandline to the lib/ directory | Xavier Leroy | 2020-05-05 | 2 | -0/+0 | |
| | | * | | Update the list of dual-licensed files | Xavier Leroy | 2020-05-05 | 1 | -2/+2 | |
| | | * | | Dual-license aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v} | Xavier Leroy | 2020-05-05 | 3 | -0/+9 | |
| | | * | | Import ListNotations explicitly | Xavier Leroy | 2020-05-04 | 1 | -0/+1 | |
| | | * | | Revert "Do not use the list notation `[]`" | Xavier Leroy | 2020-05-04 | 1 | -8/+8 | |
| | | * | | Do not use the list notation `[]` | Xavier Leroy | 2020-05-04 | 1 | -8/+8 | |
| | | * | | Do not use "Declare Scope", introduced in Coq 8.10 only | Xavier Leroy | 2020-05-04 | 1 | -1/+0 | |
| | | * | | Coq-MenhirLib: explicit import ListNotations (#354) | Jacques-Henri Jourdan | 2020-05-04 | 7 | -4/+12 | |
| | | * | | Install "compcert.config" file along the Coq development | Xavier Leroy | 2020-04-29 | 2 | -1/+19 | |
| | | * | | Updated .gitignore | Bernhard Schommer | 2020-04-27 | 1 | -0/+1 | |
| | | * | | Simplify the generation of driver/Version.ml | Bernhard Schommer | 2020-04-27 | 1 | -3/+8 | |
| | | * | | Move reserved_registers to CPragmas. | Bernhard Schommer | 2020-04-20 | 4 | -8/+8 | |
| | | * | | Support for coq 8.11.1. | Bernhard Schommer | 2020-04-20 | 1 | -2/+2 | |
| | | * | | Check for errors after each pass. | Bernhard Schommer | 2020-04-20 | 1 | -1/+8 | |
| | | * | | Added warning for packed composite with bitfields. | Bernhard Schommer | 2020-04-20 | 1 | -0/+2 | |
| | | * | | Add location to transform functions. | Bernhard Schommer | 2020-04-20 | 4 | -28/+28 | |
| * | | | | start checking for bugs | David Monniaux | 2020-12-02 | 2 | -3/+116 | |
| * | | | | attempt at initial analysis | David Monniaux | 2020-12-02 | 1 | -1/+35 | |
| * | | | | cond_depends_on | David Monniaux | 2020-12-02 | 3 | -21/+21 | |
| * | | | | simpl -> cbn | David Monniaux | 2020-12-02 | 1 | -9/+9 | |
| * | | | | cond_depends_on_memory for KVX | David Monniaux | 2020-12-02 | 1 | -4/+17 | |
| * | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3 | David Monniaux | 2020-12-02 | 79 | -731/+10580 | |
| |\ \ \ \ | | |_|/ | |/| | | ||||||
| | * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | Cyril SIX | 2020-12-01 | 6 | -11/+161 | |
| | |\ \ \ | ||||||
| | * | | | | Ignore loopback edges on tail-duplicate | Cyril SIX | 2020-12-01 | 1 | -0/+2 | |
| | * | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-24 | 13 | -31/+343 | |
| | |\ \ \ \ | ||||||
| | * | | | | | prepass scheduling proof finished ! | Sylvain Boulmé | 2020-11-20 | 1 | -24/+56 | |
| | * | | | | | merge nouveau tunneling | David Monniaux | 2020-11-19 | 1 | -1/+1 | |
| | * | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-19 | 8 | -270/+728 | |
| | |\ \ \ \ \ | ||||||
| | * | | | | | | seval_builtin_sval_preserved | David Monniaux | 2020-11-17 | 1 | -1/+4 | |
| | * | | | | | | a little lemma on list of builtins | David Monniaux | 2020-11-17 | 1 | -2/+15 | |
| | * | | | | | | there remains two tricky cases | David Monniaux | 2020-11-16 | 1 | -3/+14 | |
| | * | | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-06 | 2 | -27/+32 | |
| | |\ \ \ \ \ \ | | | |_|_|/ / | | |/| | | | | ||||||
| | * | | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-05 | 5 | -31/+114 | |
| | |\ \ \ \ \ \ | ||||||
| | * | | | | | | | disable debug printing in scheduler | David Monniaux | 2020-11-04 | 2 | -7/+9 | |
| | * | | | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-04 | 1 | -1/+2 | |
| | |\ \ \ \ \ \ \ | ||||||
| | * \ \ \ \ \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-03 | 7 | -36/+121 | |
| | |\ \ \ \ \ \ \ \ | ||||||
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |