1. 07 Jul, 2015 1 commit
  2. 20 Mar, 2015 1 commit
  3. 14 Mar, 2015 1 commit
    • Xavier Leroy's avatar
      Improve performance and configurability for the StructReturn pass. · 67e8b783
      Xavier Leroy authored
      configure: special ABI value for IA32/MacOSX and PowerPC/Linux
      cparser/Machine: special config for PowerPC/Linux
      cparser/StructReturn: generate better code for return-as-int
      driver/Clflags, driver/Driver: add options -fstruct-return=<convention>
        and -fstruct-passing=<convention> to simplify testing
  4. 27 Jan, 2015 1 commit
    • Xavier Leroy's avatar
      ABI compatibility for struct/union function arguments passed by value. · e096fa7a
      Xavier Leroy authored
      The passing of struct/union arguments by value implemented in the verified
      part of CompCert is not compatible with the ARM, PowerPC and x86 ABI.
      Here we enrich the StructReturn source-to-source emulation pass
      so that it implements the calling conventions defined in these ABIs.
      Plus: for x86, implement the returning of struct/union results by value
      in a way compatible with the ABI.
  5. 22 Jan, 2015 1 commit
    • Xavier Leroy's avatar
      Delay reads from !Machine.config before it is properly initialized. · 1e97bb4f
      Xavier Leroy authored
      Several definitions in Cutil and elsewhere were accessing the default
      value of !Machine.config, before it is properly initialized in Driver.
      Delay evaluation of these definitions, and initialize Machine.config
      to nonsensical values so that lack of initialization is caught early
      (e.g. in Cutil.find_matching_*_kind).
      Also, following up on commit [3b8a094d], don't use "wchar_t" typedef
      to type wide string literals, even if this typedef is in scope.
      The risk here is to hide an inconsistency between "wchar_t"'s definition
      in standard headers and CompCert's built-in definition.
  6. 30 Dec, 2014 1 commit
    • Xavier Leroy's avatar
      PR#6: fix handling of wchar_t and assignments from wide string literals. · 3b8a094d
      Xavier Leroy authored
      - cparser/Machine indicates whether wchar_t is signed or not
        (it is signed int in Linux and BSD, but unsigned short in Win32)
      - The type of a wide string literal is "wchar_t *" if the typedef "wchar_t"
        exists in the environment (e.g. after #include <stddef.h>).  Only if
        wchar_t is not defined do we use the default from Machine.
      - Permit initialization of any integer array from a wide string literal,
        not just an array of wchar_t.
  7. 12 Jan, 2014 1 commit
  8. 20 Dec, 2013 1 commit
  9. 29 Apr, 2013 1 commit
  10. 26 Nov, 2011 1 commit
  11. 10 Mar, 2011 1 commit
  12. 03 Mar, 2010 1 commit