Skip to content

Commit eb87bd0

Browse files
Petr BauchPetr Bauch
authored andcommitted
Add precondition where appropriate
1 parent 67220e0 commit eb87bd0

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

gnat2goto/driver/tree_walk.adb

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,8 @@ package body Tree_Walk is
3030
procedure Add_Entity_Substitution (E : Entity_Id; Subst : Irep);
3131

3232
procedure Append_Declare_And_Init
33-
(Symbol : Irep; Value : Irep; Block : Irep; Source_Loc : Source_Ptr);
33+
(Symbol : Irep; Value : Irep; Block : Irep; Source_Loc : Source_Ptr)
34+
with Pre => Kind (Value) in Class_Expr;
3435

3536
procedure Declare_Itype (Ty : Entity_Id);
3637

@@ -61,7 +62,7 @@ package body Tree_Walk is
6162
function Do_Assignment_Statement (N : Node_Id) return Irep
6263
with Pre => Nkind (N) = N_Assignment_Statement,
6364
Post => Kind (Do_Assignment_Statement'Result) in
64-
I_Code_Assign;
65+
I_Code_Assign | I_Code_Block;
6566

6667
function Do_Bare_Range_Constraint (Range_Expr : Node_Id; Underlying : Irep)
6768
return Irep

0 commit comments

Comments
 (0)