ext2: Somewhat finish proofs
diff --git a/src/filo-fs-ext2.ads b/src/filo-fs-ext2.ads
index c48ee93..1757da8 100644
--- a/src/filo-fs-ext2.ads
+++ b/src/filo-fs-ext2.ads
@@ -24,7 +24,7 @@
Success : out Boolean)
with
Pre => Is_Mounted (State),
- Post => Success = Is_Open (State);
+ Post => (if Success then Is_Open (State) else Is_Mounted (State));
procedure Close (State : in out T)
with
@@ -37,7 +37,7 @@
Buf : out Buffer_Type;
Len : out Natural)
with
- Pre => Is_Open (State),
+ Pre => Is_Open (State) and Buf'Length > 0,
Post => Is_Open (State);
private