Description
Per discussion with John, we intended that if 3C is not allowed to write a file F per its canWrite
check (based on the -base-dir
option), it should constrain the annotations in the file not to change. Otherwise, 3C may make changes to other files that depend on changes it generated for F that are silently discarded, and the other files may be uncompilable as a result. But the constraining isn't actually implemented; I thought this code was doing it, but it actually serves an unrelated purpose of generating some statistics. This issue is to implement the constraining.
Update: The most common cases have been fixed in #391. This issue is left open for the tail of unhandled cases and is tentatively labeled "unusual c code - low priority"; we'll remove that label (or file a more specific issue) if someone's actual work is affected by an unhandled case.
A related issue that I'll include here: If this test fails, meaning that we have a modified rewrite buffer for a file we weren't supposed to change, then something is wrong. I hope to be able to make this an assertion error, although conceivably there could be cases where 3C makes a non-substantive change to the file and we would have to try to find a way to assert that the change was non-substantive before discarding it. Update: This was made an error diagnostic, not an assertion error, because of the known unhandled cases.