|[ < ]||[ > ]||[ << ]||[ Up ]||[ >> ]||[Top]||[Contents]||[Index]||[ ? ]|
The use of several libraries at the same time via the common interface and the managers associated to each library raises the problem of typing. Look at the following code:
ap_manager_t* manpk = pk_manager_alloc(true); /* manager for Polka */ ap_manager_t* manoct = oct_manager_alloc(); /* manager for octagon */ ap_abstract0_t* abs1 = ap_abstract_top(manpk,3,3); ap_abstract0_t* abs2 = ap_abstract_top(manoct,3,3); bool b = ap_abstract0_is_eq(manoct,abs1,abs2); /* Problem: the effective function called (octagon_is_eq) expects abs1 to be an octagon, and not a polyhedron ! */ ap_abstract0_t* abs3 = ap_abstract_top(manoct,3,3); abstract0_meet_with(manpk,abs2,abs3); /* Problem: the effective function called (pk_meet_with) expects abs2 and abs3 to be polyhedra, but they are octagons */
There is actually no static typing, as
manager_t are abstract types shared by the different
libraries. Types are thus dynamically checked by the interface.
Notice that the use of C++ and inheritance would not solve
directly the problem, if functions of the interface are methods of
the manager; one would have:
ap_manager_t* manpk = pk_manager_alloc(true); /* manager for Polka, effective type pk_manager_t* */ ap_manager_t* manoct = oct_manager_alloc(); /* manager for octagon, effective type oct_manager_t* */ ap_abstract0_t* abs1 = manpk->abstract_top(3,3); /* effective type: poly_t */ ap_abstract0_t* abs2 = manoct->abstract_top(3,3); /* effective type: oct_t */ bool b = manoct->abstract0_is_eq(abs1,abs2); /* No static typing possible: manpk->abstract0_is_eq and manoct->abstract0_is_eq should have the same signature (otherwise one cannot interchange manpk and manoct in the code), which means that abs1 and abs2 are supposed to be of type abstract0_t* */ */
Currently, only the OCaml polymorphic type system allows to solve elegantly this problem.