Skip to content
  • Fonenantsoa Maurica's avatar
    Extend Interval, Typing and Translate: · ad8d968c
    Fonenantsoa Maurica authored and Julien Signoles's avatar Julien Signoles committed
      - 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
    ad8d968c