-
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