CONTRACTS: add doc for loop assigns inference #4
Conversation
|
Suggestion for future: doc changes like this should always be reviewed by at least one user, in addition to the CBMC development team themselves. There is a danger that the development team "know too much" about all this stuff, and don't appreciate how clueless newbie users (i.e. like me!) really are! I will take a look at this one. |
| 2. collecting assigns targets with local-may-alias analysis, | ||
| 3. assigns targets widening. | ||
|
|
||
| We do the function inlining first so that we can infer those assigns targets |
There was a problem hiding this comment.
What if the body of a called unit is not available, but that unit does have contracts, and --replace-all-with-contract has been specified? If you can't inline what happens? Can you get the info you need from the contract of the called unit alone?
|
Please see review comments above. I will try this on a few functions from mlkem-native and see what we get. |
|
Reopened in as diffblue#8516. |
This PR add an example, explanation, and limitation of the loop assigns inference used in DFCC contracts.