/*
 * ValidFunctionOpDeclChecker.java
 * ---------------------------------
 * Copyright (c) 2017
 * RESOLVE Software Research Group
 * School of Computing
 * Clemson University
 * All rights reserved.
 * ---------------------------------
 * This file is subject to the terms and conditions defined in
 * file 'LICENSE.txt', which is part of this source code package.
 */
package edu.clemson.cs.rsrg.typeandpopulate.sanitychecking;

import edu.clemson.cs.rsrg.absyn.declarations.operationdecl.OperationDec;
import edu.clemson.cs.rsrg.parsing.data.Location;
import edu.clemson.cs.rsrg.statushandling.exception.SourceErrorException;

/**
 * <p>This is a sanity checker for making sure the {@link OperationDec}
 * is valid function operation declaration.</p>
 *
 * @author Yu-Shan Sun
 * @version 1.0
 */
public class ValidFunctionOpDeclChecker {

    // ===========================================================
    // Member Fields
    // ===========================================================

    /** <p>The function operation declaration to be checked.</p> */
    private final OperationDec MyFunctionOperationDec;

    // ===========================================================
    // Constructors
    // ===========================================================

    /**
     * <p>Creates a sanity checker for checking the various different criteria
     * for being a valid function operation declaration.</p>
     *
     * @param functionOperation The associated function operation declaration.
     */
    public ValidFunctionOpDeclChecker(OperationDec functionOperation) {
        MyFunctionOperationDec = functionOperation;
    }

    // ===========================================================
    // Public Methods
    // ===========================================================

    /**
     * <p>Checks to see if the provided {@link OperationDec} is a
     * valid function operation declaration. A valid function
     * operation declaration must be of the form:
     * {@code <FuncOpDeclName> = <Expression/Value>}</p>
     *
     * @throws SourceErrorException This is thrown if it is not a valid
     * function operation declaration. The message will indicate why it is
     * not valid.
     */
    public final void checkFunctionOpDecl() {}

}
@@ -499,16 +499,267 @@
 ionDec;%0A
+import edu.clemson.cs.rsrg.absyn.expressions.Exp;%0Aimport edu.clemson.cs.rsrg.absyn.expressions.mathexpr.EqualsExp;%0Aimport edu.clemson.cs.rsrg.absyn.expressions.mathexpr.EqualsExp.Operator;%0Aimport edu.clemson.cs.rsrg.absyn.expressions.mathexpr.VarExp;%0A
 import e
@@ -800,16 +800,16 @@
 cation;%0A
-
 import e
@@ -1343,17 +1343,17 @@
 tionDec 
-M
+m
 yFunctio
@@ -1845,17 +1845,17 @@
         
-M
+m
 yFunctio
@@ -2223,18 +2223,53 @@
 on must 
-be
+have an %7B@code ensures%7D clause%0A     *
  of the 
@@ -2273,23 +2273,16 @@
 he form:
-%0A     *
  %7B@code 
@@ -2319,16 +2319,17 @@
 /Value%3E%7D
+.
 %3C/p%3E%0A   
@@ -2497,32 +2497,32 @@
  valid.%0A     */%0A
-
     public final
@@ -2550,12 +2550,534 @@
 Decl() %7B
+%0A        Location funcOpLoc = myFunctionOperationDec.getLocation();%0A        String funcOpName = myFunctionOperationDec.getName().getName();%0A        Exp ensuresExp = myFunctionOperationDec.getEnsures().getAssertionExp();%0A%0A        // 1. Make sure we don't have %22ensures true%22%0A        if (!VarExp.isLiteralTrue(ensuresExp)) %7B%0A            %0A        %7D%0A        else %7B%0A            throw new SourceErrorException(%22Function operation: %22 + funcOpName + %22 cannot have 'ensures true;' as its specification.%22, funcOpLoc);%0A        %7D%0A    
 %7D%0A%0A%7D

No ensures true