Coin under -d does not call the correct version of a function

[frankpfenning]

After reading this file

int test(int x) //@requires x > 0; //@ensures \result < 0; ;

int test(int x) //@requires x >= 0; //@ensures \result <= 0; { return -x; }

int main () { return test(0); }

calls to 'test(n)' should check both sets of contracts, as the call in 'main' does. coin calls the function 'test' directly, not its latest version. Bug is probably in dyn-check.sml, or the way this is called from coin.

[robsimmons]

I fixed some bugs with internal names in coin, but as far as I can tell the coin toplevel under -d is now correctly transforming code and checking these contracts. You can look at --print-codes to get the inside scoop.

Frank, because I never managed to replicate, can you confirm that this works as of r211?

[frankpfenning]

Yes, it works as of r211. Will close.

The stack trace still prints the internal function stack frames, which is okay for advanced debugging but might confuse students. A small improvement might be to hide these frames whose function name is internal.