Module Frama_c_kernel.Destructors

retrieve local variables with __fc_destructor attribute and add the appropriate calls to the corresponding destructor function when we exit the scope of the variable.

Argument of the attribute can take the following forms:

• AStr f, where f is the name of the function to call.
• ACons (f, [AInt n]), where f is the name of the function to call and n an argument that will be passed to f in addition to the variable. Will be used for destructing local C++ arrays.
• AAddrOf a where a is of the form above, to indicate that the destructor should be given the address of the variable and not the variable directly