The meaning of the attribute is to tell iContractTask what
file to *read* and pass it on to iContract, so iContract
knows for which classes it should instrument, and what
assertions
It's possible to have the task create it when it's
specified, and it doesn't exist, but I don't see the point.
We can only make assumptions about what to put in it. (Ex:
enable pre, post, invariant everywhere). This is actually
what iContractTask does, but it does so using the -
mpre,post,inv flag instead.
I suggest we reject this bug report, unless I misunderstood
what you meant ;-)
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Logged In: YES
user_id=49846
The meaning of the attribute is to tell iContractTask what
file to *read* and pass it on to iContract, so iContract
knows for which classes it should instrument, and what
assertions
It's possible to have the task create it when it's
specified, and it doesn't exist, but I don't see the point.
We can only make assumptions about what to put in it. (Ex:
enable pre, post, invariant everywhere). This is actually
what iContractTask does, but it does so using the -
mpre,post,inv flag instead.
I suggest we reject this bug report, unless I misunderstood
what you meant ;-)