1. 03 Jul, 2015 1 commit
  2. 02 Jul, 2015 3 commits
  3. 01 Jul, 2015 2 commits
  4. 30 Jun, 2015 2 commits
  5. 26 Jun, 2015 9 commits
  6. 25 Jun, 2015 1 commit
  7. 24 Jun, 2015 1 commit
  8. 22 Jun, 2015 3 commits
  9. 18 Jun, 2015 1 commit
  10. 12 Jun, 2015 1 commit
  11. 11 Jun, 2015 5 commits
  12. 10 Jun, 2015 1 commit
  13. 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
  14. 07 Jun, 2015 1 commit
  15. 06 Jun, 2015 1 commit
  16. 05 Jun, 2015 1 commit
  17. 31 May, 2015 1 commit
  18. 22 May, 2015 2 commits
  19. 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
  20. 18 May, 2015 1 commit
  21. 14 May, 2015 1 commit