- 09 May, 2015 1 commit
-
-
Xavier Leroy authored
- Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting
-
- 07 May, 2015 1 commit
-
-
Bernhard Schommer authored
-
- 06 May, 2015 1 commit
-
-
Xavier Leroy authored
-
- 30 Apr, 2015 2 commits
-
-
Xavier Leroy authored
-
Xavier Leroy authored
Detect uses of anonymous structs/unions (a C2011 feature and GCC extension) and produce a diagnostic instead of ignoring them.
-
- 28 Apr, 2015 3 commits
-
-
Xavier Leroy authored
-
Xavier Leroy authored
Bitfield improvements continued: perform bitfield expansion before unblocking; improve translation of bitfield initializers and compound literals.
-
Xavier Leroy authored
Bitfields: better translation of initializers and compound literals; run this pass before unblocking. Transform.stmt: extend with ability to treat unblocked code. test/regression: more bitfield tests.
-
- 25 Apr, 2015 1 commit
-
-
Xavier Leroy authored
Also: spurious '\n' in C2C.warning.
-
- 23 Apr, 2015 4 commits
-
-
Xavier Leroy authored
-
Xavier Leroy authored
-
Xavier Leroy authored
-
Xavier Leroy authored
-
- 22 Apr, 2015 2 commits
-
-
Xavier Leroy authored
GCC-style extended inline asm. The subset implemented is: - zero or one output - output constraints "=r" (to register) or "=m" (to memory) - zero, one or several inputs - input constraints "r" (in register), "m" (in memory), "i" and "n" (compile-time integer constant) - clobbered registers (the 3rd argument) - both anonymous (%3) and named (%[name]) operands - modifiers %R and %Q to refer to the most significant / least significant part of a register pair holding a 64-bit integer. (Undocumented GCC ARM feature.) All asm statements are treated as "volatile", possibly modifying memory and condition codes.
-
Xavier Leroy authored
We can ignore alternatives as long as one of the constraints we handle (r, m, i, n) is there.
-
- 21 Apr, 2015 6 commits
-
-
Xavier Leroy authored
-
Xavier Leroy authored
-
Xavier Leroy authored
-
Xavier Leroy authored
-
Xavier Leroy authored
-
Xavier Leroy authored
- support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml
-
- 17 Apr, 2015 2 commits
-
-
Xavier Leroy authored
-
Xavier Leroy authored
-
- 16 Apr, 2015 2 commits
-
-
Bernhard Schommer authored
-
Bernhard Schommer authored
-
- 15 Apr, 2015 1 commit
-
-
Bernhard Schommer authored
Added the Dwarf v2 debugging information for global variables and functions for the Diab Backend.
-
- 14 Apr, 2015 3 commits
-
-
Bernhard Schommer authored
-
Bernhard Schommer authored
-
Bernhard Schommer authored
-
- 10 Apr, 2015 1 commit
-
-
Xavier Leroy authored
As opposed to the default "gnu99" mode, the C99 mode turns off a number of GNU-isms in standard header files like those of glibc.
-
- 06 Apr, 2015 3 commits
-
-
Xavier Leroy authored
Detect (and reject with an error) preprocessing numbers that are not valid integer or floating constants.
-
Xavier Leroy authored
-
Xavier Leroy authored
-
- 04 Apr, 2015 3 commits
-
-
Bernhard Schommer authored
-
Bernhard Schommer authored
-
Xavier Leroy authored
-
- 02 Apr, 2015 4 commits
-
-
Bernhard Schommer authored
-
Bernhard Schommer authored
-
Bernhard Schommer authored
Cosmetic: README in MarkDown
-
Bernhard Schommer authored
Ccompuimm now depends on the memory, this is needed to proof the Lemma op_depends_on_memory_correct.
-