1. 26 Jun, 2015 4 commits
  2. 25 Jun, 2015 1 commit
  3. 24 Jun, 2015 1 commit
  4. 22 Jun, 2015 1 commit
  5. 12 Jun, 2015 1 commit
  6. 11 Jun, 2015 5 commits
  7. 08 Jun, 2015 1 commit
    • Xavier Leroy's avatar
      Merge pull request #43 from AbsInt/standard-headers · 744dc278
      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. 
      744dc278
  8. 07 Jun, 2015 1 commit
  9. 06 Jun, 2015 1 commit
  10. 05 Jun, 2015 1 commit
  11. 31 May, 2015 1 commit
  12. 22 May, 2015 2 commits
  13. 21 May, 2015 1 commit
    • Xavier Leroy's avatar
      Ctyping: better typing of conditional expressions. · b686f8df
      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.
      b686f8df
  14. 18 May, 2015 1 commit
  15. 14 May, 2015 2 commits
  16. 13 May, 2015 1 commit
  17. 09 May, 2015 3 commits
  18. 07 May, 2015 1 commit
  19. 06 May, 2015 1 commit
  20. 30 Apr, 2015 2 commits
  21. 28 Apr, 2015 3 commits
  22. 26 Apr, 2015 1 commit
  23. 25 Apr, 2015 2 commits
  24. 23 Apr, 2015 2 commits