sig val array : Cil_types.kernel_function States.array end