1 /********************************************************************************
2 *
3 * Copyright (c) 2008 Fujitsu Services Ltd.
4 *
5 * Author: Nick Battle
6 *
7 * This file is part of VDMJ.
8 *
9 * VDMJ is free software: you can redistribute it and/or modify
10 * it under the terms of the GNU General Public License as published by
11 * the Free Software Foundation, either version 3 of the License, or
12 * (at your option) any later version.
13 *
14 * VDMJ is distributed in the hope that it will be useful,
15 * but WITHOUT ANY WARRANTY; without even the implied warranty of
16 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17 * GNU General Public License for more details.
18 *
19 * You should have received a copy of the GNU General Public License
20 * along with VDMJ. If not, see <http://www.gnu.org/licenses/>.
21 *
22 ******************************************************************************/
23
24 package org.overturetool.vdmj.statements;
25
26 import org.overturetool.vdmj.expressions.Expression;
27 import org.overturetool.vdmj.lex.LexLocation;
28 import org.overturetool.vdmj.pog.POContextStack;
29 import org.overturetool.vdmj.pog.ProofObligationList;
30 import org.overturetool.vdmj.runtime.Context;
31 import org.overturetool.vdmj.typechecker.Environment;
32 import org.overturetool.vdmj.typechecker.NameScope;
33 import org.overturetool.vdmj.types.Type;
34 import org.overturetool.vdmj.types.TypeSet;
35 import org.overturetool.vdmj.types.UnknownType;
36 import org.overturetool.vdmj.types.VoidReturnType;
37 import org.overturetool.vdmj.values.Value;
38 import org.overturetool.vdmj.values.VoidReturnValue;
39
40 public class ReturnStatement extends Statement
41 {
42 private static final long serialVersionUID = 1L;
43 public final Expression expression;
44
45 public ReturnStatement(LexLocation location)
46 {
47 super(location);
48 this.expression = null;
49 }
50
51 public ReturnStatement(LexLocation location, Expression expression)
52 {
53 super(location);
54 this.expression = expression;
55 }
56
57 @Override
58 public String toString()
59 {
60 return "return" + (expression == null ? "" : " (" + expression + ")");
61 }
62
63 @Override
64 public String kind()
65 {
66 return "return";
67 }
68
69 @Override
70 public Type typeCheck(Environment env, NameScope scope)
71 {
72 if (expression == null)
73 {
74 return new VoidReturnType(location);
75 }
76 else
77 {
78 return expression.typeCheck(env, null, scope);
79 }
80 }
81
82 @Override
83 public TypeSet exitCheck()
84 {
85 if (expression != null)
86 {
87
88 return new TypeSet(new UnknownType(location));
89 }
90 else
91 {
92 return super.exitCheck();
93 }
94 }
95
96 @Override
97 public Value eval(Context ctxt)
98 {
99 breakpoint.check(location, ctxt);
100
101 if (expression == null)
102 {
103 return new VoidReturnValue();
104 }
105 else
106 {
107 return expression.eval(ctxt);
108 }
109 }
110
111 @Override
112 public Expression findExpression(int lineno)
113 {
114 return expression == null ? null : expression.findExpression(lineno);
115 }
116
117 @Override
118 public ProofObligationList getProofObligations(POContextStack ctxt)
119 {
120 ProofObligationList obligations = new ProofObligationList();
121
122 if (expression != null)
123 {
124 obligations.addAll(expression.getProofObligations(ctxt));
125 }
126
127 return obligations;
128 }
129 }