src/main/java/com/amazonaws/encryptionsdk/internal/PrimitivesParser.java (3 lines):
	- line 192: // @ // left as TODO because OpenJML/Specs does not have sufficiently detailed
	- line 196: // @//    assignable TODO ...
	- line 197: // @//    ensures    TODO ...


src/main/java/com/amazonaws/encryptionsdk/model/KeyBlob.java (3 lines):
	- line 575: // @ private normal_behavior  // TODO: this behavior is a temporary workaround
	- line 611: // @ private normal_behavior  // TODO: this behavior is a temporary workaround
	- line 644: // @ private normal_behavior  // TODO: this behavior is a temporary workaround