Skip to content
  • xleroy's avatar
    Merge of the clightgen branch: · 85397590
    xleroy authored
    - Alternate semantics for Clight where function parameters are temporaries,
      not variables
    - New pass SimplLocals that turns non-addressed local variables into
      temporaries
    - Simplified Csharpminor, Cshmgen and Cminorgen accordingly
    - SimplExpr starts its temporaries above variable names, therefoe
      Cminorgen no longer needs to encode variable names and temps names.
    - Simplified Cminor parser & printer, as well as Errors, accordingly.
    - New tool clightgen to produce Clight AST in Coq-parsable .v files.
    - Removed side condition "return type is void" on rules skip_seq
      in the semantics of CompCert C, Clight, C#minor, Cminor.
    - Adapted RTLgenproof accordingly (now uses a memory extension).
    
    
    git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2083 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
    85397590