2 ms·
You were clear, and you were wrong. The annotations are checked like I said, you cannot break the guarantees using them. If they're incorrect they won't pass ve
by afdbcreid 17d ago
You were clear, and you were wrong. The annotations are checked like I said, you cannot break the guarantees using them. If they're incorrect they won't pass verification. They just help the verifier.
- MeetingsBrowser 17d agoSorry I’ll try to put it simply. Programmer intends to write code that does Y, but writes code that does X. Then they make the same mistake again and write an annotation that verifies the function does X. Verification passes, but the code does the wrong thing.