- 22 Jun, 2015 3 commits
-
-
Bernhard Schommer authored
-
Bernhard Schommer authored
-
Bernhard Schommer authored
-
- 17 Jun, 2015 1 commit
-
-
Bernhard Schommer authored
-
- 12 Jun, 2015 1 commit
-
-
Xavier Leroy authored
-
- 11 Jun, 2015 5 commits
-
-
Xavier Leroy authored
-
Xavier Leroy authored
Otherwise we get too many errors on glibc's standard headers. A real error will occur when the anonymous struct/union is accessed.
-
Xavier Leroy authored
-
Xavier Leroy authored
-
Xavier Leroy authored
-
- 08 Jun, 2015 1 commit
-
-
Xavier Leroy authored
Merge of the "standard-headers" branch. This provides CompCert-compatible implementations of the following standard headers: float.h, stdarg.h, stdbool.h, stddef.h, varargs.h. These are the headers that are provided by GCC, Clang, and TCC. Other standard headers are provided by Glibc and similar C standard libraries. So far in CompCert we rely on the headers provided by whatever C compiler is installed on the host platform. This causes some difficulties that this branch addresses: 1- Diab C's stdarg.h is not compatible with CompCert 2- On IA32 and PowerPC, CompCert's "long double" type differs from the "long double" type specified by the ABI. Hence, the platform's float.h gives "long double" parameters that do not match CompCert.
-
- 07 Jun, 2015 1 commit
-
-
Xavier Leroy authored
As noticed by R. Krebbers, an inductive type for external worlds implies that all sequences of program-world interactions are finite, which is not the case.
-
- 06 Jun, 2015 1 commit
-
-
Xavier Leroy authored
Error if, in the same scope, a typedef is redefined as a variable, or a variable is redefined as a typedef.
-
- 05 Jun, 2015 1 commit
-
-
Xavier Leroy authored
-
- 31 May, 2015 1 commit
-
-
Bernhard Schommer authored
Allow the option -o to be also the prefix of the file name for compability with different build systems.
-
- 29 May, 2015 2 commits
-
-
Bernhard Schommer authored
-
Bernhard Schommer authored
-
- 22 May, 2015 2 commits
-
-
Xavier Leroy authored
Use this info in printing function types for Csyntax and Clight.
-
Xavier Leroy authored
-
- 21 May, 2015 2 commits
-
-
Bernhard Schommer authored
-
Xavier Leroy authored
Ctyping: define a typechecker for whole programs. Csyntax: introduce the type "pre-program" (non-dependent). C2C: use Ctyping.econdition instead of Ctyping.econdition'. Note: Ctyping.typecheck_program could be used as the first step in the verified compilation pipeline. Then, retyping would no longer be performed in C2C. We keep it this way (for the time being) because retyping errors are reported more precisely in C2C than in Ctyping.
-
- 19 May, 2015 1 commit
-
-
Bernhard Schommer authored
-
- 18 May, 2015 3 commits
-
-
Bernhard Schommer authored
-
Bernhard Schommer authored
-
Bernhard Schommer authored
-
- 14 May, 2015 2 commits
-
-
Bernhard Schommer authored
-
Bernhard Schommer authored
-
- 13 May, 2015 1 commit
-
-
Bernhard Schommer authored
Changed the enter_or_refine_ident function to produce an error if a non-static declaration is followed by a static declaration/definition.
-
- 09 May, 2015 3 commits
-
-
Xavier Leroy authored
-
Xavier Leroy authored
-
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 2 commits
-
-
Bernhard Schommer authored
-
Bernhard Schommer authored
-
- 06 May, 2015 2 commits
-
-
Bernhard Schommer authored
Moved the information needed from the atoms to the ASM printer and removed unused information from the json dump.
-
Xavier Leroy authored
-
- 05 May, 2015 2 commits
-
-
Bernhard Schommer authored
-
Bernhard Schommer 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 1 commit
-
-
Xavier Leroy authored
-