Menu

#94 ZVCG inconsistent state after exception

open
5
2012-01-25
2012-01-25
Leo Freitas
No

I was doing an example and generated FSB VCs. All is okay. Then I added refinement annotations and generated VCs again. But I'd forgotten to
add the retrieve schema and an exception was raised. All is okay.

Then I ask to regenerate VCs and some VCs get either duplicated or with the version within the file exactly like the one "inserted at cursor", yet there
is the errror

Description Resource Path Location Type
The paragraph differs from the one generated by Verification Condition Generator. Replace with generated. test2.zed /Test line 295 CZT VCG Problem

Clues?

Discussion


Log in to post a comment.