Open
Description
Today it is perfectly legal to run
goto-instrument --enforce-contract foo a.out a.out
goto-instrument --enforce-contract bar a.out a.out
And by "legal" I mean that goto-instrument
does not complain about enforcing a second contract. However the semantics break. Without dfcc I think it fails during checking and with dfcc it fails because of an arity mismatch (the lambda holding the contract clauses has one argument less than the function it attaches to, because that function has already been instrumented and the frame argument been added).
It would be better if goto-instrument
could detect that it is being invoked again and report it as an error, informing the user that only one contract may be enforced at a time.