Confusion between two function-types instantiations in an indirect call

[necto]

When I have a generic function type, and two instantiations for different type-arguments, VeriFast searches for a wrong is_... predicate instance:

typedef int fun/*@ <t>(predicate (void*;t) pred) @*/(void* p);
//@ requires pred(p, ?x);
//@ ensures pred(p, x);

int f1(void* p)
//@ requires integer(p, ?x);
//@ ensures integer(p, x);
{
  return 0;
}

int f2(void* p)
//@ requires character(p, ?x);
//@ ensures character(p, x);
{
  return 1;
}

void caller()
//@ requires true;
//@ ensures true;
{
  /*@ produce_function_pointer_chunk fun<int>(f1)(integer)(x)
      {
        call();
      }
    @*/
  /*@ produce_function_pointer_chunk fun<char>(f2)(character)(x)
      {
        call();
      }
    @*/
  fun* a = f1;
  fun* b = f2;
  int c = '.';
  int x = a(&c); //<-- here
}

The report is: "No matching heap chunks: is_fun(f1, _)"

While it should really call using is_fun<int>(f1,_)

[btj]

You can work around this by hiding the is_fun<char>(f2, _) chunk before the call of f1, by wrapping it inside a helper predicate (which you can define as a block-local predicate inside caller so that it can use local variables).

[necto]

That works, thank you.