+
+ lastekind = KINVALID;
+
+ fprintf(fout, ";; Library constraints\n");
+ for (i = 0; i < utab->nentries; i++)
+ {
+ uentry thisentry = utab->entries[i];
+
+ if (uentry_isFunction (thisentry) )
+ {
+ constraintList preconditions;
+ constraintList postconditions;
+
+ preconditions = uentry_getFcnPreconditions (thisentry);
+ postconditions = uentry_getFcnPostconditions (thisentry);
+
+ if ( constraintList_isDefined(preconditions) ||
+ constraintList_isDefined(postconditions) )
+ {
+ fprintf(fout,"%s\n", uentry_rawName(thisentry) );
+ if (constraintList_isDefined(preconditions) )
+ {
+ fprintf(fout,"pre:\n");
+ constraintList_dump(preconditions, fout);
+ fprintf (fout, ";; end precondition constraints\n" );
+ constraintList_free(preconditions);
+ }
+ else
+ {
+ fprintf(fout,"pre:EMPTY\n");
+ }
+ if (constraintList_isDefined(postconditions) )
+ {
+ fprintf(fout,"post:\n");
+ constraintList_dump(postconditions, fout);
+ fprintf (fout, ";; end precondition constraints\n" );
+ constraintList_free(postconditions);
+ }
+ else
+ {
+ fprintf(fout,"post:EMPTY\n");
+ }
+ }
+
+ }
+ }
+
+
+