2.0.4 Parameters of the analysis

The analysis done by the CINV tool is parametrized by the following inputs:

• Domain: The abstract domain used to represent heap segments. This domain is used by the global domain of Shapes. The following domains are implemented in CINV:

  LSUM-PRD

  the domain of sums over heap segments which is a Cartesian product of a domain for lengths of segments and a domain for data of segments.
  

  LSUM-REL

  the domain of sums over heap segments where lengths and data are put together.
  

  UCONS

  the domain of universally constrained heap segments; this domain is parametrized by the set of patterns used by the universally quantified constraints. These patterns have the following codes:

  P11

  \forall y in n
  

  P12

  \forall y1 in n, y2 in m, y1=y2
  

  P21

  \forall y1,y2 in n, y1<y2
  

  P211

  \forall y1,y2 in n, y1 <1 y2

• Anonymous number: The computation of the post abstract transformer is parameterized by the maximum number of anonymous in the heap graph. In CINV, this number is obtained from the following two parameters:

  max_anon

  the maximum number of anonymous nodes in a heap segment, and
  

  segm_anon

  the number of segments shall divide the number of anonymous nodes.

  These two parameters shall be given (in this order) by the file cinv.txt in the directory chosen for the execution of CINV.