Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8 | David Monniaux | 2020-11-18 | 1 | -4/+6 |
|\ | |||||
| * | Updates for release 3.8v3.8 | Xavier Leroy | 2020-11-16 | 1 | -4/+6 |
| | | |||||
* | | link on Cyril's short video | Sylvain Boulmé | 2020-10-19 | 1 | -2/+2 |
| | | |||||
* | | update the title of our paper | Sylvain Boulmé | 2020-10-07 | 1 | -2/+2 |
| | | |||||
* | | links to the impure library on github | Sylvain Boulmé | 2020-07-31 | 1 | -1/+1 |
| | | |||||
* | | Improving Coqdoc on abstractbb | Sylvain Boulmé | 2020-07-31 | 1 | -1/+1 |
| | | |||||
* | | Improving the coqdoc | Sylvain Boulmé | 2020-07-29 | 1 | -5/+5 |
| | | |||||
* | | automatic date in the html index | Sylvain Boulmé | 2020-05-28 | 1 | -1/+1 |
| | | |||||
* | | source url in the doc | Sylvain Boulmé | 2020-05-27 | 1 | -2/+4 |
| | | |||||
* | | link to the HAL preprint | Sylvain Boulmé | 2020-05-27 | 1 | -2/+6 |
| | | |||||
* | | k1c -> kvx changes | David Monniaux | 2020-05-26 | 1 | -37/+37 |
| | | |||||
* | | fix index-mppa_k1c.html | Sylvain Boulmé | 2020-05-11 | 1 | -1/+1 |
| | | |||||
* | | updating the html index for mppa-k1c | Sylvain Boulmé | 2020-05-10 | 1 | -45/+27 |
| | | | | | | | | NOTE: This file has been copied from the one of pldi-artefact branch. | ||||
* | | Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-work | Cyril SIX | 2020-04-01 | 1 | -1/+3 |
|\| | |||||
| * | Updates for release 3.7 | Xavier Leroy | 2020-03-31 | 1 | -1/+3 |
| | | |||||
* | | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2019-09-20 | 1 | -2/+3 |
|\| | | | | | | | mppa-work-upstream-merge | ||||
| * | Update for release 3.6v3.6 | Xavier Leroy | 2019-09-17 | 1 | -2/+3 |
| | | |||||
* | | Merge branch 'mppa-work' of ↵ | David Monniaux | 2019-09-10 | 1 | -0/+380 |
|\ \ | |/ |/| | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work | ||||
| * | a dedicated entry-point to the doc of Coq sources | Sylvain Boulmé | 2019-09-03 | 1 | -0/+380 |
| | | |||||
* | | Update man page. | Bernhard Schommer | 2019-09-02 | 1 | -1/+1 |
|/ | | | | Unused-variables is disabled by default. | ||||
* | More precise description of '-O0' and 'non-linear-cond-expr' | Michael Schmidt | 2019-07-10 | 1 | -1/+2 |
| | |||||
* | Update synonymous list for -O0, add new named warning class | Michael Schmidt | 2019-07-05 | 1 | -1/+6 |
| | |||||
* | Update documentation of -Obranchless | Xavier Leroy | 2019-07-05 | 1 | -6/+8 |
| | | | | Updated man page + better usage message. | ||||
* | Updated man page. | Bernhard Schommer | 2019-06-17 | 1 | -0/+10 |
| | |||||
* | Fix misspellings in messages, man pages, and comments | Xavier Leroy | 2019-05-31 | 1 | -1/+1 |
| | | | | | | This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream. | ||||
* | Added options -fcommon and -fno-common (#164) | Bernhard Schommer | 2019-05-10 | 1 | -0/+6 |
| | | | | | | | | | | The option -fcommon controls whether uninitialized global variables are placed in the COMMON section. If the option is given in the negated form, -fno-common, variables are not placed in the COMMON section. They are placed in the same sections as gcc does. If the variables are not placed in the COMMON section merging of tentative definitions is inhibited and multiple definitions lead to a linker error, as it does for gcc. | ||||
* | Check for alignment of command-line switches. | Bernhard Schommer | 2019-05-10 | 1 | -3/+3 |
| | | | | | | Add a check for alignment on command-line switches `-falign-*`. The check is similar to the one for the alignment attribute and ensures that only powers of two can be specified. | ||||
* | Update HTML doc for release 3.5 | Xavier Leroy | 2019-02-27 | 1 | -1/+1 |
| | |||||
* | Fix some URLs in the first page of the Coq HTML documentation (#263) | Andre | 2019-01-22 | 1 | -5/+5 |
| | | | | Links to machine-specific modules were garbled during editing. | ||||
* | Updates for release 3.4v3.4 | Xavier Leroy | 2018-09-17 | 1 | -1/+1 |
| | |||||
* | document new named warning class 'reduced-alignment', bug 23389 | Michael Schmidt | 2018-09-04 | 1 | -0/+4 |
| | |||||
* | Document new named warning for tentative static definitions with incomplete ↵ | Michael Schmidt | 2018-08-21 | 1 | -0/+4 |
| | | | | type, bug 23377 | ||||
* | Document new named warning for flexible arrays, bug 23324 | Michael Schmidt | 2018-08-21 | 1 | -1/+1 |
| | |||||
* | Document new named warning for flexible arrays, bug 23324 | Michael Schmidt | 2018-08-21 | 1 | -0/+4 |
| | |||||
* | Remove undocumented option. | Bernhard Schommer | 2018-08-07 | 1 | -4/+0 |
| | | | | | The option -doptions was never document and no longer works. Bug 19775 | ||||
* | Typo in Ctyping entry | Xavier Leroy | 2018-06-17 | 1 | -1/+1 |
| | |||||
* | bug 23325, document recently introduced named warnings | Michael Schmidt | 2018-06-05 | 1 | -2/+2 |
| | |||||
* | bug 23325, document recently introduced named warnings | Michael Schmidt | 2018-06-05 | 1 | -3/+3 |
| | |||||
* | bug 23325, document recently introduced named warnings | Michael Schmidt | 2018-06-05 | 1 | -1/+1 |
| | |||||
* | bug 23325, document recently introduced named warnings | Michael Schmidt | 2018-06-05 | 1 | -4/+28 |
| | |||||
* | bug 23325, document changed default for c11 named warning | Michael Schmidt | 2018-06-05 | 1 | -1/+1 |
| | |||||
* | Use the standalone coq2html tool to generate the HTML documentation | Xavier Leroy | 2018-06-01 | 5 | -752/+115 |
| | | | | | coq2html is now a standalone project (https://github.com/xavierleroy/coq2html) packaged as coq-coq2html in OPAM-Coq. | ||||
* | Update for release 3.3v3.3 | Xavier Leroy | 2018-05-30 | 1 | -1/+1 |
| | |||||
* | coq2html: use OCaml's alternate string literals for multi-line strings | Xavier Leroy | 2018-05-30 | 1 | -15/+15 |
| | |||||
* | Update manpage for new warning name class | Michael Schmidt | 2018-03-08 | 1 | -0/+4 |
| | |||||
* | Preparations for release 3.2 | Xavier Leroy | 2018-01-13 | 1 | -4/+4 |
| | |||||
* | Mention the RISC-V port as well | Xavier Leroy | 2018-01-13 | 1 | -1/+1 |
| | |||||
* | Update man page for new Diab target option | Michael Schmidt | 2018-01-08 | 1 | -6/+8 |
| | |||||
* | Update man page for new Diab target option | Michael Schmidt | 2018-01-08 | 1 | -0/+6 |
| | |||||
* | Inlining of static functions which are only called once. (#37) | Bernhard Schommer | 2017-12-07 | 1 | -0/+5 |
| | | | | | | | | | New inlining heuristic for static functions. Static functions that are only called once can always be inlined, since they can be removed safely after inlining and no call prologue, epilogue, as well as register saving and needs to be generated. |