Skip to content
  • Fonenantsoa Maurica's avatar
    Addresses Julien's review no.1: · c9f1976f
    Fonenantsoa Maurica authored
    - No superfluous white space
    - No camel case
    - No unauthorized open
    - Longic_const.tinteger -> Cil.lone, Cil.lzero
    - lscope -> Lscope.t
    - lscope becomes abstract
    - 'with non-void logic scope' -> 'on purely logical variables'
    - Make lscope be part of env
    - Discard all the translation in a new module: At_with_lscope
    - No extra variable for size
    - Cil.(theMachine.typeOfSizeOf) instead of Cil.intType
    - No superfluous block for storing_loops
    - mem_infos -> memory_infos
    - Prevent GMP result (actually already done previously)
    - record for malloc and free
    - H_malloc_free = Cil_datatype.Fundec.Hashtbl
    - dedicated insert_malloc_and_free_stmts in Visit
    - Kernel_function.is_entry_point for testing main function
    - no visit in term_has_lv_from_vi and effective_lscope_from_pot
    - term_has_lv_from_vi moved to Misc
    - Passing kf to add_malloc_and_free_stmt instead of fundec
    - Less @ during the insertion of free stmts
    - ty_array -> ty_ptr
    - Typos
    - Comments on:
      - Exported functions in MLIs
      - Computation of pre in put_block_at_label
      - Use of global scope for Env.Varname.get
      - Description of mk_storing_loops
      - New binding in mk_storing_loops
      - Description of effective_lscope_from_pred_or_term
      - Motivation of the over-approximation on t_size
    c9f1976f