+static void
+reflectEnsuresClause (uentry le, exprNode f, exprNodeList args)
+{
+ DPRINTF (("Reflect ensures clause: %s(%s) / %s / %s",
+ exprNode_unparse (f), exprNodeList_unparse (args),
+ uentry_unparseFull (le),
+ stateClauseList_unparse (uentry_getStateClauseList (le))));
+
+ if (uentry_isValid (le) && uentry_isFunction (le))
+ {
+ stateClauseList sclauses = uentry_getStateClauseList (le);
+
+ if (stateClauseList_isDefined (sclauses))
+ {
+ DPRINTF (("Reflect ensures: %s / %s / %s",
+ uentry_unparse (le),
+ exprNode_unparse (f), exprNodeList_unparse (args)));
+
+ stateClauseList_elements (sclauses, cl)
+ {
+ if (stateClause_hasEnsures (cl))
+ {
+ /* Same in usymtab.c:1904 */
+ if (stateClause_setsMetaState (cl))
+ {
+ qual q = stateClause_getMetaQual (cl);
+ annotationInfo ainfo = qual_getAnnotationInfo (q);
+ metaStateInfo minfo = annotationInfo_getState (ainfo);
+ cstring key = metaStateInfo_getName (minfo);
+ int mvalue = annotationInfo_getValue (ainfo);
+
+ sRefSet osrs = sRefSet_undefined;
+ sRefSet srs;
+
+ if (stateClause_isGlobal (cl))
+ {
+ srs = sRefSet_single (usymtab_lookupGlobalMarker ());
+ osrs = srs;
+ }
+ else
+ {
+ srs = stateClause_getRefs (cl);
+ }
+
+ DPRINTF (("Reflect ensures clause: %s", stateClause_unparse (cl)));
+
+
+ DPRINTF (("Sets meta state! %s", stateClause_unparse (cl)));
+
+ sRefSet_elements (srs, sel)
+ {
+ sRef s;
+
+ if (sRef_isResult (sRef_getRootBase (sel)))
+ {
+ ; /*@i423 what do we do about results */
+ }
+ else
+ {
+ s = sRef_fixBaseParam (sel, args);
+ DPRINTF (("Reflecting state clause on: %s / %s",
+ sRef_unparse (sel), sRef_unparse (s)));
+
+ sRef_setMetaStateValueComplete (s, key, mvalue, exprNode_loc (f));
+ }
+ } end_sRefSet_elements;
+
+ sRefSet_free (osrs);
+ }
+ else
+ {
+ sRefSet srs = stateClause_getRefs (cl);
+ sRefModVal modf = stateClause_getEnsuresFunction (cl);
+ int eparam = stateClause_getStateParameter (cl);
+
+ DPRINTF (("Reflect after clause: %s / %s",
+ stateClause_unparse (cl),
+ sRefSet_unparse (srs)));
+
+ sRefSet_elements (srs, sel)
+ {
+ sRef s;
+
+ DPRINTF (("elements: %s", sRef_unparse (sel)));
+ DPRINTF (("elements: %s", sRef_unparseFull (sel)));
+
+ if (sRef_isResult (sRef_getRootBase (sel)))
+ {
+ ; /*@i423 what do we do about results */
+ }
+ else
+ {
+ s = sRef_fixBaseParam (sel, args);
+
+ DPRINTF (("elements: %s", sRef_unparse (s)));
+ DPRINTF (("elements: %s", sRef_unparseFull (s)));
+
+ DPRINTF (("Reflecting state clause on: %s / %s",
+ sRef_unparse (sel), sRef_unparse (s)));
+
+ modf (s, eparam, exprNode_loc (f));
+ }
+ } end_sRefSet_elements;
+ }
+ }
+ } end_stateClauseList_elements ;
+
+ }
+ }
+}
+
+static void
+checkRequiresClause (uentry le, exprNode f, exprNodeList args)
+{
+ DPRINTF (("Check requires clause: %s(%s) / %s / %s",
+ exprNode_unparse (f), exprNodeList_unparse (args),
+ uentry_unparseFull (le),
+ stateClauseList_unparse (uentry_getStateClauseList (le))));
+
+ if (uentry_isValid (le) && uentry_isFunction (le))
+ {
+ stateClauseList sclauses = uentry_getStateClauseList (le);
+
+ if (stateClauseList_isDefined (sclauses))
+ {
+ DPRINTF (("Check requires: %s / %s / %s",
+ uentry_unparse (le),
+ exprNode_unparse (f), exprNodeList_unparse (args)));
+
+ stateClauseList_elements (sclauses, cl)
+ {
+ DPRINTF (("Check clause: %s / %s",
+ stateClause_unparse (cl),
+ bool_unparse (stateClause_hasRequires (cl))));
+
+ if (stateClause_hasRequires (cl))
+ {
+ sRefSet osrs = sRefSet_undefined;
+ sRefSet srs;
+
+ if (stateClause_isGlobal (cl))
+ {
+ srs = sRefSet_single (usymtab_lookupGlobalMarker ());
+ osrs = srs;
+ }
+ else
+ {
+ srs = stateClause_getRefs (cl);
+ }
+
+ DPRINTF (("Refs: %s", sRefSet_unparse (srs)));
+
+ if (stateClause_setsMetaState (cl))
+ {
+ qual q = stateClause_getMetaQual (cl);
+ annotationInfo ainfo = qual_getAnnotationInfo (q);
+ metaStateInfo minfo = annotationInfo_getState (ainfo);
+ cstring key = metaStateInfo_getName (minfo);
+ int mvalue = annotationInfo_getValue (ainfo);
+
+ DPRINTF (("Requires meta state! %s = %d", key, mvalue));
+
+ sRefSet_elements (srs, sel)
+ {
+ sRef s = sRef_fixBaseParam (sel, args);
+
+ if (sRef_isResult (sRef_getRootBase (sel)))
+ {
+ ; /*@i423 what do we do about results */
+ }
+ else
+ {
+ DPRINTF (("Checking state clause on: %s / %s / %s = %d",
+ sRef_unparseFull (sel), sRef_unparseFull (s),
+ key, mvalue));
+
+ if (!sRef_checkMetaStateValue (s, key, mvalue))
+ {
+ DPRINTF (("HERE: %s", sRef_unparse (s)));
+ if (optgenerror
+ (FLG_STATETRANSFER,
+ message
+ ("Requires clause of called function %q not satisfied%q (state is %q): %q",
+ uentry_getName (le),
+ sRef_isGlobalMarker (s)
+ ? message ("")
+ : message (" by %q", sRef_unparse (s)),
+ stateValue_unparseValue (sRef_getMetaStateValue (s, key),
+ minfo),
+ stateClause_unparse (cl)),
+ exprNode_loc (f)))
+ {
+ sRef_showAliasInfo (s);
+ }
+ else
+ {
+ DPRINTF (("Error supressed!"));
+ DPRINTF (("Loc: %s", fileloc_unparse (exprNode_loc (f))));
+ DPRINTF (("Context supress: %s",
+ bool_unparse (context_suppressFlagMsg (FLG_STATETRANSFER, exprNode_loc (f)))));
+ }
+ }
+ }
+ } end_sRefSet_elements;
+ }
+ else
+ {
+ sRefModVal modf = stateClause_getRequiresBodyFunction (cl);
+ int eparam = stateClause_getStateParameter (cl);
+
+ DPRINTF (("Reflect after clause: %s / %s",
+ stateClause_unparse (cl),
+ sRefSet_unparse (srs)));
+
+ sRefSet_elements (srs, sel)
+ {
+ sRef s;
+
+ DPRINTF (("elements: %s", sRef_unparse (sel)));
+ DPRINTF (("elements: %s", sRef_unparseFull (sel)));
+
+ s = sRef_fixBaseParam (sel, args);
+
+ DPRINTF (("elements: %s", sRef_unparse (s)));
+ DPRINTF (("elements: %s", sRef_unparseFull (s)));
+
+ if (sRef_isResult (sRef_getRootBase (sel)))
+ {
+ ; /*@i423 what do we do about results */
+ }
+ else
+ {
+ DPRINTF (("Reflecting state clause on: %s / %s",
+ sRef_unparse (sel), sRef_unparse (s)));
+
+ modf (s, eparam, exprNode_loc (f));
+ }
+ } end_sRefSet_elements;
+ }
+
+ sRefSet_free (osrs);
+ }
+ } end_stateClauseList_elements ;
+ }
+ }
+}
+