Updated html and word versions of the manual

[splint.git] / src / Headers / constraintResolve.h

diff --git a/src/Headers/constraintResolve.h b/src/Headers/constraintResolve.h
index 29775ab2fb0b0649b337c13686351b7cd6971fc8..5a28ef91d9a56ca548759ba2333dc4b0442b2948 100644 (file)
--- a/src/Headers/constraintResolve.h
+++ b/src/Headers/constraintResolve.h
@@ -1,22 +1,40 @@
 
-extern constraintList reflectChanges (constraintList pre2, constraintList post1);
-extern constraint substitute (constraint c, constraintList p);
-//extern constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new);
-extern bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2);
-extern bool satifies (constraint pre, constraint post);
+extern /*@only@*/ constraintList constraintList_reflectChanges(/*@observer@*/ /*@temp@*/ constraintList p_pre2, /*@observer@*/ /*@temp@*/ constraintList p_post1);
 
-extern bool resolve ( /*@observer@*/ constraint c,  /*@observer@*/ constraintList p);
-extern constraintList reflectChangesEnsures (constraintList pre2, constraintList post1);
-extern constraint constraint_simplify (constraint c);
 
-extern constraintList constraintList_fixConflicts (constraintList list1, constraintList list2);
+/* tries to resolve constraints in List p_pre2 using post1 */
+/*@only@*/ extern constraintList constraintList_reflectChangesFreePre (/*@only@*/ constraintList p_pre2, /*@observer@*/ /*@temp@*/ constraintList p_post1);
 
-extern constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2);
+extern /*@only@*/ constraint constraint_substitute (/*@temp@*/ /*@observer@*/ constraint p_c, /*@temp@*/ /*@observer@*/ constraintList p_p);
 
-extern constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2);
+/* extern constraint constraint_searchandreplace (constraint p_c, constraintExpr old, constraintExpr new); */
 
-bool constraint_isAlwaysTrue (constraint c);
-constraintList constraintList_mergeRequires (constraintList list1, constraintList list2);
-constraintList reflectChangesOr (constraintList pre2, constraintList post1);
+extern bool constraintList_resolve (/*@temp@*/ /*@observer@*/ constraint p_c,  /*@temp@*/ /*@observer@*/ constraintList p_p);
+
+extern constraint constraint_simplify ( /*@returned@*/ constraint p_c);
+
+extern /*@only@*/ constraintList constraintList_fixConflicts (constraintList p_list1, constraintList p_list2);
+
+extern constraintList constraintList_subsumeEnsures (constraintList p_list1, constraintList p_list2);
+
+extern constraintList constraintList_mergeEnsures (/*observer@*/ /*@temp@*/ constraintList p_list1, /*@observer@*/ /*@temp@*/ constraintList p_list2);
+
+/*@only@*/ constraintList constraintList_mergeEnsuresFreeFirst (/*@only@*/ constraintList p_list1, /*@observer@*/ /*@temp@*/ constraintList p_list2);
+
+
+bool constraint_isAlwaysTrue (/*@observer@*/ /*@temp@*/ constraint p_c);
+
+/*@only@*/ constraintList constraintList_mergeRequires (/*@observer@*/ /*@temp@*/ constraintList p_list1,/*@observer@*/ /*@temp@*/ constraintList p_list2);
+
+/*@only@*/ constraintList constraintList_mergeRequiresFreeFirst (/*@only@*/constraintList p_list1,/*@observer@*/ /*@temp@*/ constraintList p_list2);
+
+
+
+constraintList constraintList_reflectChangesOr (constraintList p_pre2, constraintList p_post1);
+
+/*@only@*/ constraintList constraintList_substitute (constraintList p_target, /*2observer@*/ constraintList p_subList);
+
+/*@only@*/ constraintList constraintList_substituteFreeTarget (/*@only@*/ constraintList p_target, /*@observer@*/ /*@temp@*/ constraintList p_subList);
+
+extern void exprNode_mergeResolve (exprNode p_parent, exprNode p_child1, exprNode p_child2);
 
-constraintList constraintList_substitute (constraintList target, constraintList subList);