+ if (optgenerror
+ (FLG_INCONDEFS,
+ message
+ ("Postconditions for %q redeclared. Dropping previous postcondition: %q",
+ uentry_getName (spec),
+ functionConstraint_unparse (spec->info->fcn->postconditions)),
+ uentry_whereLast (def)))
+ {
+ uentry_showWhereSpecified (spec);
+ }
+
+ functionConstraint_free (spec->info->fcn->postconditions);
+ spec->info->fcn->postconditions = def->info->fcn->postconditions;
+ def->info->fcn->postconditions = functionConstraint_undefined;