Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

  1. 08 May, 2021 1 commit
  2. 21 Feb, 2020 1 commit
    • Xavier Leroy's avatar
      Refine the type of function results in AST.signature · be0b1872
      Xavier Leroy authored
      Before it was "option typ".  Now it is a proper inductive type
      that can also express small integer types (8/16-bit unsigned/signed integers).
      
      One benefit is that external functions get more precise types that
      control better their return values.  As a consequence,
      the CompCert C type preservation property now holds unconditionally,
      without extra typing hypotheses on external functions.
      be0b1872
  3. 08 Aug, 2019 1 commit
    • Xavier Leroy's avatar
      AArch64 port · 7cdd676d
      Xavier Leroy authored
      This commit adds a back-end for the AArch64 architecture, namely ARMv8
      in 64-bit mode.
      7cdd676d
  4. 17 Jul, 2019 1 commit
    • Xavier Leroy's avatar
      Give formal semantics to some built-in functions and run-time functions · d08b0807
      Xavier Leroy authored
      This commit adds mechanisms to
      - recognize certain built-in and run-time functions by name and signature;
      - associate semantics to these functions, as a partial function from
        list of values to values;
      - interpret external calls to these functions according to this semantics
        (pure function from values to values, memory unchanged, no observable
        events in the trace);
      - external calls to unknown built-in and run-time functions remain
        interpreted as generating observable events and possibly changing
        memory, like before.
      
      The description of the built-ins is split into a target-independent
      part (in common/Builtins0.v) and a target-specific part (in
      $ARCH/Builtins1.v).
      
      Instruction selection uses the new mechanism in order to
      - recognize some built-in functions and turn them into operations
        of the target processor.  Currently, this is done for
        __builtin_sel and __builtin_fabs; more to come.
      - remove the axioms about int64 helper functions from the standard
        library.  More precisely, the behavior of these functions is
        still axiomatized, but now it is specified using the more general
        machinery introduced in this commit, rather than ad-hoc axioms
        in backend/SplitLongproof.
      
      The only built-ins currently described are __builtin_fsqrt (for all platforms)
      and __builtin_fmin / __builtin_fmax (for x86).  More built-ins will be
      added later.
      d08b0807
  5. 09 Mar, 2018 1 commit
  6. 07 Nov, 2015 1 commit
  7. 08 Oct, 2015 1 commit
  8. 30 Sep, 2015 1 commit
  9. 29 Apr, 2014 1 commit
  10. 03 Mar, 2010 1 commit
  11. 30 Dec, 2008 1 commit
  12. 27 Jan, 2008 1 commit
  13. 17 Jul, 2006 1 commit