GitLab

Fonenantsoa Maurica authored Jan 08, 2019 and Julien Signoles committed Aug 02, 2019

  - Interval:
    - Not_an_integer -> Is_a_real|Not_a_number.
    - infer -> infer_with_real
      because Not_a_number has priority over Is_a_real
    - Ival.bottom when Is_a_real
      because the interval is for integers
  - Typing:
    - integer_ty -> number_ty=Cty|Gmpz|Libr|Nan
    - Other -> 'Other (Oreal|Onan)'
  - Translate:
    Encode real constants into strings:
      - **NO** conversion to float-point type
      - strnum_ty=StrZ|StrR|Not_a_strnum
        for tracking the type of the string
Add Libr:
  - Gmpz -> Gmp=Gmpz+Gmpq
  - Libr=ref to Gmpq
Add Gmpq builtins:
  - Custom mini-gmp -> libgmp
    because mini-gmp has no support for Q
  - Add arithmetic over Q in e_acsl_gmp_api.h
Misc:
  - dec_to_frac: decimal expansion to fractional representation
    because decimal expansion is interpreted as double by Gmpq
Tests:
  - BTS 1307 has an assertion wrongly evaluated, fixed
  - Add tests/gmp/reals.c
THE MOST IMPORTANT TODO:
  - Completely hide the library for numbers (currently Gmp)
    inside Libr: Typing, Env and Translate should only know
    Libr and never directly call Gmp.
    This is crucial for extending E-ACSL in the future
    (eg: Gmp has no support for elementary functions), and
    also for using it as part of an abstract compiler
    (eg: with Fldlib)
    For the time being, in Translate,
    we have something as ugly as:
      let init_set =
        if Libr.is_t ty then Libr.init_set
        else Gmp.init_set

Fixes Issue 69: unsound translation when bounds for quantified variables are bigger than their types

Patrick Baudin authored Oct 02, 2018 and Julien Signoles committed Oct 15, 2018

  internal: use of hdrck for targets headers, check-headers and src-distrib
  external: reviewed target headers

- Stack of varinfos instead of list of varinfos
- stmts_block -> block_to_stmt, which results in less @
- fold_right instead of map+ref
- Optimizing with SkipChildren
- Useless parentheses. Typo. Indentation. No if not then else. begin...end instead of (...) for imperative constructs.

- Less lengthy closure in index_from_sizes_and_shifts
- String on multiple lines.
- Comment for extend_stmt_in_place
- Detail pattern matching in vblock
- List.exists instead of List.find
- mem instead of find in At_with_lscope.remove_all
- effective_lscope -> is_used

 - Sad goodbye to insert_before_element_under_condition
 - ~label instead of ~pre
 - No superfluous Env.Varname.get
 - Gmp only allowed
 - Dataflow analysis allowed
 - Using exception for term_has_lv_from_vi
 - Fix incorrect assert false from effective_lscope_from_pred_or_term
 - fold_left for index_from_sizes_and_shifts

MAJOR:
- malloc and free
  - Distinct tables for malloc and free
  - Efficient insertion of free and malloc
  - Remove entries for malloc and free when they are not needed anymore
- Using kf instead of fundec
- Using closure of vi_at: not (straightforwardly) possible
- Logic scope:
  - No Lscope.top
  - Proper reseting of the lscope
  - Proper binding of logic variables
  - Module Env.Logic_scope
- Comment for the over-approximation of t_size

STYLE:
- No useless new lines
- Spaces
- Parentheses
- Latex style for formula in comment of index_from_sizes_and_shifts
- match -> function
- Logical variable -> logic variable
- Renaming:
  - add_to_lscope ->  extend_lscope
  - memory_infos_from_quantifs -> sizes_and_shifts_from_quantifs
  - res -> sizes_and_shifts, memory_infos -> sizes_and_shifts
- Typos
- Forward references at the end of the mli
- Consistent ordering of arguments inside Lscope API

OTHERS:
- Auxiliary function append_block_of_env_to_block
- Squash pattern matching of mk_storing_loops
- No Interval.infer in to_exp
- Refactoring of pre_from_label
- pi_beta_j with fold_left
- No superfluous env for sizes_and_shifts_from_quantifs
- More efficient accumulator for computing size
- Squash pattern matching of sizes_and_shifts_from_quantifs
- No superfluous option for get_lscope_var
- Better definition of effective_lscope_from_pred_or_term
- Using List.find for defining get_lscope_var
- Do not export get_lscope_var
- Lscope.empty () -> Lscope.empty

- 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

 - Date format in Changelog
 - No code generation in the original project
 - \valid_read(&(t.j) + (1..3)) is valid
 - addresses -> pointers

  - No superfluous patterns
  - Using Cil.charPtrType
  - call_for_unsupported_constructs as closure given to mmodel_call_with_ranges
  - Style:
    - Indendation
    - No superfluous begin..end
    - Parentheses
    - Spaces

 - Remove double warning for arithmetic over pointers
 - Not yet: size of memory area in GMP
 - Typing of Trange
 - Squashing pattern matchings
 - Use of has_set_as_index
 - No is_offset_of_array
 - Using exception in is_range_free
 - Using `call f`
 - Logic.is_set_type instead of catching Failure
 - Logic.const.taddrof
 - &t, instead of &t[0], is sufficient for arrays
 - No useless rec
 - Typos, useless parentheses, no camel case, comments, indentation

- Interval inference and typing
- Multi-dimensional arrays with ranges as indexes:
  - If the only range is the last index -> single call to builtin
  - Else -> not yet "arithmetic over set of pointers" (requires Mmodel modification)
- Tests for struct
- Richer pattern matching instead of is_trange
- has_range -> Misc.is_range_free
- Using Cil_const.make_logic_var_kind, Logic_const.taddrof, Logic_const.type_of_element and Logic_utils.mk_cast
- [elt] @ list -> elt :: list
- Options.fatal -> Options.abort
- Comments:
  - On the Range Elimination operation
  - Describing the formula for the range-free term
  - Describing mmodel_call_with_ranges and mmodel_call_default