aboutsummaryrefslogtreecommitdiffstats
path: root/common/AST.v
Commit message (Expand)AuthorAgeFilesLines
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-4/+5
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-8/+8
|\
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-3/+3
| * Changed cc_varargs to an option typeBernhard Schommer2020-12-251-5/+5
* | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-1/+1
|\|
| * Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-211-1/+1
* | print hashesDavid Monniaux2020-04-081-2/+3
* | begin installing profilingDavid Monniaux2020-04-081-4/+5
* | added EF_profilingDavid Monniaux2020-04-081-1/+9
* | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-031-1/+28
|\ \ | |/ |/|
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-021-1/+18
| |\
| | * Ibuiltin proofCyril SIX2019-10-041-1/+18
| * | more proofs going throughDavid Monniaux2019-09-051-0/+1
| * | moved trapping_mode to a more appropriate placeDavid Monniaux2019-09-031-0/+9
| |/
* / Refine the type of function results in AST.signatureXavier Leroy2020-02-211-20/+59
|/
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-311-2/+2
* New support for inserting ais-annotations.Bernhard Schommer2017-10-191-7/+7
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-061-14/+7
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-7/+7
* Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-131-3/+3
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-12/+26
* Unwanted partial constant propagation in 64-bit integer arguments to builtinsXavier Leroy2016-07-081-1/+1
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-171-1/+56
* AST: extend and adapt to the new linking framework.Xavier Leroy2016-03-061-460/+116
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-37/+37
* Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-12/+8
* Added versions of the tranform_* functions in AST to work with functionsBernhard Schommer2015-10-081-1/+216
* Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-221-10/+10
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-58/+85
* In AST.calling_conventions, record whether the original C function was "old-s...Xavier Leroy2015-05-221-3/+4
* Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-091-2/+2
* Support for GCC-style extended asm, continued:Xavier Leroy2015-04-211-3/+4
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-171-3/+3
* Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-16/+57
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-0/+9
* Record public global definitions via field "prog_public" in AST.program.Xavier Leroy2014-11-241-3/+25
* Merge of "newspilling" branch:xleroy2014-07-231-33/+35
* Type-checking of builtin volatile write Mfloat32 was too strict, causing type...xleroy2014-03-241-2/+2
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-5/+2
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-281-16/+34
* Merge of the float32 branch: xleroy2013-05-191-4/+69
* Refactoring: move definition of chunk_of_type to AST.v.xleroy2013-05-061-0/+10
* Coq-defined equality functions for Allocation.xleroy2013-05-011-3/+20
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-15/+24
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-2/+4
* Constant propagation within __builtin_annot.xleroy2013-02-241-3/+15
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-6/+6
* Support for inline assembly (asm statements).xleroy2012-12-181-1/+9
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-253/+169
generated by cgit (git 2.34.1) at 2024-05-09 11:58:24 +0000