/*
-** constraintList.c
+** constraint.c
*/
//#define DEBUGPRINT 1
# include "exprChecks.h"
# include "aliasChecks.h"
# include "exprNodeSList.h"
-//# include "exprData.i"
/*@i33*/
/*@-fcnuse*/
/*@-assignexpose*/
-/*@notnull@*/ constraint constraint_makeNew (void);
+/*@access exprNode @*/
-constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant)
+static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c);
+
+
+static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
+ /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
-{
- char *t;
- int c;
- constraint ret;
- ret = constraint_makeNew();
- llassert (sRef_isValid(x) );
- if (!sRef_isValid(x))
- return ret;
+/* constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant) */
+
+/* { */
+/* char *t; */
+/* int c; */
+/* constraint ret; */
+/* ret = constraint_makeNew(); */
+/* llassert (sRef_isValid(x) ); */
+/* if (!sRef_isValid(x)) */
+/* return ret; */
- ret->lexpr = constraintExpr_makeTermsRef (x);
- #warning fix abstraction
+/* ret->lexpr = constraintExpr_makeTermsRef (x); */
+/* #warning fix abstraction */
- if (relOp.tok == GE_OP)
- ret->ar = GTE;
- else if (relOp.tok == LE_OP)
- ret->ar = LTE;
- else if (relOp.tok == EQ_OP)
- ret->ar = EQ;
- else
- llfatalbug(message ("Unsupported relational operator") );
+/* if (relOp.tok == GE_OP) */
+/* ret->ar = GTE; */
+/* else if (relOp.tok == LE_OP) */
+/* ret->ar = LTE; */
+/* else if (relOp.tok == EQ_OP) */
+/* ret->ar = EQ; */
+/* else */
+/* llfatalbug(message ("Unsupported relational operator") ); */
- t = cstring_toCharsSafe (exprNode_unparse(cconstant));
- c = atoi( t );
- ret->expr = constraintExpr_makeIntLiteral (c);
+/* t = cstring_toCharsSafe (exprNode_unparse(cconstant)); */
+/* c = atoi( t ); */
+/* ret->expr = constraintExpr_makeIntLiteral (c); */
- ret->post = TRUE;
- // ret->orig = ret;
- DPRINTF(("GENERATED CONSTRAINT:"));
- DPRINTF( (message ("%s", constraint_print(ret) ) ) );
- return ret;
+/* ret->post = TRUE; */
+/* // ret->orig = ret; */
+/* DPRINTF(("GENERATED CONSTRAINT:")); */
+/* DPRINTF( (message ("%s", constraint_print(ret) ) ) ); */
+/* return ret; */
+/* } */
+
+
+static void
+advanceField (char **s)
+{
+ checkChar (s, '@');
}
-constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
-
+
+
+constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
{
char *t;
int c;
constraint ret;
ret = constraint_makeNew();
llassert (l!=NULL);
- if (!l)
- return ret;
-
-
+
ret->lexpr = constraintExpr_copy (l);
- #warning fix abstraction
+
if (relOp.tok == GE_OP)
ret->ar = GTE;
return ret;
}
+bool constraint_same (constraint c1, constraint c2)
+{
+
+ if (c1->ar != c2->ar)
+ return FALSE;
+
+ if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
+ return FALSE;
+
+ if (!constraintExpr_similar (c1->expr, c2->expr) )
+ return FALSE;
+
+ return TRUE;
+}
constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
{
constraint ret;
ret = constraint_makeNew();
llassert (l !=NULL);
- if (!l)
- return ret;
-
ret->lexpr = constraintExpr_copy (l);
- #warning fix abstraction
if (relOp.tok == GE_OP)
ret->ar = GTE;
ret->expr = constraintExpr_copy (r);
ret->post = TRUE;
+
+ ret->orig = constraint_copy(ret);
+
+ ret = constraint_simplify (ret);
+
// ret->orig = ret;
DPRINTF(("GENERATED CONSTRAINT:"));
DPRINTF( (message ("%s", constraint_print(ret) ) ) );
constraint constraint_copy (constraint c)
{
constraint ret;
+
+ llassert (constraint_isDefined(c) );
+ // TPRINTF((message("Copying constraint %q", constraint_print) ));
+
ret = constraint_makeNew();
ret->lexpr = constraintExpr_copy (c->lexpr);
ret->ar = c->ar;
ret->orig = constraint_copy (c->orig);
else
ret->orig = NULL;
+
+ if (c->or != NULL)
+ ret->or = constraint_copy (c->or);
+ else
+ ret->or = NULL;
+
+ ret->fcnPre = c->fcnPre;
+
return ret;
}
/*like copy expect it doesn't allocate memory for the constraint*/
-void constraint_overWrite (constraint c1, constraint c2)
+void constraint_overWrite (constraint c1, constraint c2)
{
+ llassert (constraint_isDefined(c1) );
+
+ llassert (c1 != c2);
+
+ DPRINTF((message("OverWriteing constraint %q with %q", constraint_print(c1),
+ constraint_print(c2) ) ));
+
+ constraintExpr_free(c1->lexpr);
+ constraintExpr_free(c1->expr);
+
c1->lexpr = constraintExpr_copy (c2->lexpr);
c1->ar = c2->ar;
c1->expr = constraintExpr_copy (c2->expr);
c1->post = c2->post;
- /*@i33 fix this*/
+
+ if (c1->orig != NULL)
+ constraint_free (c1->orig);
+
if (c2->orig != NULL)
c1->orig = constraint_copy (c2->orig);
else
c1->orig = NULL;
- c1->generatingExpr = exprNode_fakeCopy (c2->generatingExpr );
-}
-bool constraint_resolve (/*@unused@*/ constraint c)
-{
- return FALSE;
+ /*@i33 make sure that the or is freed correctly*/
+ if (c1->or != NULL)
+ constraint_free (c1->or);
+
+ if (c2->or != NULL)
+ c1->or = constraint_copy (c2->or);
+ else
+ c1->or = NULL;
+
+ c1->fcnPre = c2->fcnPre;
+
+ c1->generatingExpr = c2->generatingExpr;
}
-/*@notnull@*/ constraint constraint_makeNew (void)
+static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
+ /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
{
constraint ret;
ret = dmalloc(sizeof (*ret) );
ret->ar = LT;
ret->post = FALSE;
ret->orig = NULL;
+ ret->or = NULL;
ret->generatingExpr = NULL;
+ ret->fcnPre = NULL;
return ret;
}
return c;
}
+constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
+{
+
+ if (c->orig != constraint_undefined)
+ {
+ c->orig = constraint_addGeneratingExpr(c->orig, e);
+ }
+ else
+ {
+ DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
+ }
+ return c;
+}
+
+constraint constraint_setFcnPre (/*@returned@*/ constraint c )
+{
+
+ if (c->orig != constraint_undefined)
+ {
+ c->orig->fcnPre = TRUE;
+ }
+ else
+ {
+ c->fcnPre = TRUE;
+ // TPRINTF(( message("Warning Setting fcnPre directly") ));
+ }
+ return c;
+}
+
+
+
+
fileloc constraint_getFileloc (constraint c)
{
- if (c->generatingExpr)
- return (exprNode_getfileloc (c->generatingExpr) );
+ if (exprNode_isDefined(c->generatingExpr) )
+ return (fileloc_copy (exprNode_getfileloc (c->generatingExpr) ) );
return (constraintExpr_getFileloc (c->lexpr) );
ret->lexpr = constraintExpr_makeMaxReadExpr(po);
ret->ar = GTE;
ret->expr = constraintExpr_makeValueExpr (ind);
+ ret->post = FALSE;
return ret;
}
ret->lexpr =constraintExpr_makeMaxSetExpr(po);
ret->ar = GTE;
- ret->expr = constraintExpr_makeValueInt (ind);
+ ret->expr = constraintExpr_makeIntLiteral (ind);
/*@i1*/return ret;
}
-constraint constraint_makeSRefSetBufferSize (sRef s, int size)
+constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
{
constraint ret = constraint_makeNew();
ret->lexpr = constraintExpr_makeSRefMaxset (s);
ret->ar = EQ;
- ret->expr = constraintExpr_makeValueInt (size);
+ ret->expr = constraintExpr_makeIntLiteral ((int)size);
ret->post = TRUE;
/*@i1*/return ret;
}
constraint ret = constraint_makeNew();
- ret->lexpr = constraintExpr_makeSRefMaxset (s);
+ ret->lexpr = constraintExpr_makeSRefMaxset ( s );
ret->ar = GTE;
- ret->expr = constraintExpr_makeValueInt (ind);
+ ret->expr = constraintExpr_makeIntLiteral (ind);
ret->post = TRUE;
/*@i1*/return ret;
}
ret->lexpr = constraintExpr_makeMaxReadExpr(po);
ret->ar = GTE;
- ret->expr = constraintExpr_makeValueInt (ind);
+ ret->expr = constraintExpr_makeIntLiteral (ind);
+ ret->post = FALSE;
return ret;
}
constraint ret = constraint_makeNew();
- ret->lexpr = constraintExpr_makeSRefMaxRead (s);
+ ret->lexpr = constraintExpr_makeSRefMaxRead (s );
ret->ar = GTE;
- ret->expr = constraintExpr_makeValueInt (ind);
+ ret->expr = constraintExpr_makeIntLiteral (ind);
ret->post = TRUE;
/*@i1*/return ret;
}
constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
{
- constraint ret = constraint_makeNew();
-
+ constraint ret;
e1 = exprNode_fakeCopy (e1);
t2 = exprNode_fakeCopy (t2);
return ret;
}
-static constraint constraint_makeEnsuresOpConstraintExpr (constraintExpr c1, constraintExpr c2, fileloc sequencePoint, arithType ar)
+static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint, arithType ar)
{
constraint ret;
exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
{
+ constraintList_free(dst->ensuresConstraints);
+ constraintList_free(dst->requiresConstraints);
+ constraintList_free(dst->trueEnsuresConstraints);
+ constraintList_free(dst->falseEnsuresConstraints);
+
dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
return dst;
}
+/* Makes the constraint e = e + f */
+constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint)
+{
+ constraintExpr x1, x2, y;
+ constraint ret;
+
+ ret = constraint_makeNew();
+
+ x1 = constraintExpr_makeValueExpr (e);
+ x2 = constraintExpr_copy(x1);
+ y = constraintExpr_makeValueExpr (f);
+
+ ret->lexpr = x1;
+ ret->ar = EQ;
+ ret->post = TRUE;
+ ret->expr = constraintExpr_makeAddExpr (x2, y);
+
+ ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+
+ return ret;
+}
+
+
+/* Makes the constraint e = e - f */
+constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint)
+{
+ constraintExpr x1, x2, y;
+ constraint ret;
+
+ ret = constraint_makeNew();
+
+ x1 = constraintExpr_makeValueExpr (e);
+ x2 = constraintExpr_copy(x1);
+ y = constraintExpr_makeValueExpr (f);
+
+ ret->lexpr = x1;
+ ret->ar = EQ;
+ ret->post = TRUE;
+ ret->expr = constraintExpr_makeSubtractExpr (x2, y);
+
+ ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+
+ return ret;
+}
+
constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
{
constraint ret = constraint_makeNew();
}
+void constraint_free (/*@only@*/ constraint c)
+{
+ llassert(constraint_isDefined (c) );
+
+
+ if (constraint_isDefined(c->orig) )
+ constraint_free (c->orig);
+ if ( constraint_isDefined(c->or) )
+ constraint_free (c->or);
+
+
+ constraintExpr_free(c->lexpr);
+ constraintExpr_free(c->expr);
+
+ c->orig = NULL;
+ c->or = NULL;
+ c->lexpr = NULL;
+ c->expr = NULL;
+
+ free (c);
+
+}
+
// constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
// {
return st;
}
+void constraint_printErrorPostCondition (constraint c, fileloc loc)
+{
+ cstring string;
+ fileloc errorLoc, temp;
+
+ string = constraint_printDetailedPostCondition (c);
+
+ errorLoc = loc;
+
+ loc = NULL;
+
+ temp = constraint_getFileloc(c);
+
+ if (fileloc_isDefined(temp) )
+ {
+ errorLoc = temp;
+ voptgenerror ( FLG_CHECKPOST, string, errorLoc);
+ fileloc_free(temp);
+ }
+ else
+ {
+ voptgenerror ( FLG_CHECKPOST, string, errorLoc);
+ }
+}
+
+
+
+
void constraint_printError (constraint c, fileloc loc)
{
cstring string;
- fileloc errorLoc;
+ fileloc errorLoc, temp;
string = constraint_printDetailed (c);
errorLoc = loc;
- if (constraint_getFileloc(c) )
- /*@-branchstate@*/
- errorLoc = constraint_getFileloc(c);
- /*@=branchstate@*/
-
- if (c->post)
+ loc = NULL;
+
+ temp = constraint_getFileloc(c);
+
+ if (fileloc_isDefined(temp) )
{
- voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
+ errorLoc = temp;
+
+ if (c->post)
+ {
+ voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
+ }
+ else
+ {
+ voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
+ }
+ fileloc_free(temp);
}
else
{
- voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
+ if (c->post)
+ {
+ voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
+ }
+ else
+ {
+ voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
+ }
}
-
}
-cstring constraint_printDetailed (constraint c)
+
+cstring constraint_printDeep (constraint c)
{
cstring st = cstring_undefined;
+ st = constraint_print(c);
+
+ if (c->orig != constraint_undefined)
+ {
+ if (!c->post)
+ {
+ if (c->orig->fcnPre)
+ st = cstring_concatFree(st, (message(" derived from %s precondition: %q", exprNode_unparse(c->orig->generatingExpr), constraint_printDeep(c->orig) )
+ ) );
+ else
+ st = cstring_concatFree(st,(message(" needed to satisfy %q",
+ constraint_printDeep(c->orig) )
+ ) );
+
+ }
+ else
+ {
+ st = cstring_concatFree(st,(message("derived from: %q",
+ constraint_printDeep(c->orig) )
+ ) );
+ }
+ }
+
+ return st;
+
+}
+
+
+static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
+{
+ cstring st = cstring_undefined;
+
+ st = message ("Unsatisfied ensures constraint condition:\nLCLint is unable to verify the constraint %q", constraint_printDeep (c) );
+
+ if (context_getFlag (FLG_CONSTRAINTLOCATION) )
+ {
+ cstring temp;
+ // llassert (c->generatingExpr);
+ temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
+ exprNode_unparse(c->generatingExpr) );
+ st = cstring_concatFree (st, temp);
+
+ if (constraint_hasMaxSet(c) )
+ {
+ temp = message ("Has MaxSet\n");
+ st = cstring_concatFree (st, temp);
+ }
+ }
+ return st;
+}
+
+cstring constraint_printDetailed (constraint c)
+{
+ cstring st = cstring_undefined;
if (!c->post)
{
- if (c->orig != NULL)
- st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisfy %s", constraint_print (c), constraint_print(c->orig) );
- else
- st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
-
+ st = message ("Unresolved constraint:\nLclint is unable to resolve %q", constraint_printDeep (c) );
}
else
{
- if (c->orig != NULL)
- st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
- else
- st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));
+ st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c) );
}
if (context_getFlag (FLG_CONSTRAINTLOCATION) )
{
cstring temp;
// llassert (c->generatingExpr);
- temp = message ("\nOriginal Generating expression %s: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
+ temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
exprNode_unparse(c->generatingExpr) );
- st = cstring_concat (st, temp);
+ st = cstring_concatFree (st, temp);
if (constraint_hasMaxSet(c) )
{
- cstring temp2;
- temp2 = message ("\nHas MaxSet\n");
- st = cstring_concat (st, temp2);
+ temp = message ("Has MaxSet\n");
+ st = cstring_concatFree (st, temp);
}
}
return st;
}
-cstring constraint_print (constraint c) /*@*/
+/*@only@*/ cstring constraint_print (constraint c) /*@*/
{
cstring st = cstring_undefined;
cstring type = cstring_undefined;
{
type = cstring_makeLiteral ("Requires: ");
}
- st = message ("%s: %s %s %s",
+ st = message ("%q: %q %q %q",
type,
constraintExpr_print (c->lexpr),
arithType_print(c->ar),
return st;
}
+cstring constraint_printOr (constraint c) /*@*/
+{
+ cstring ret;
+ constraint temp;
+
+ ret = cstring_undefined;
+ temp = c;
+
+ ret = cstring_concatFree (ret, constraint_print(temp) );
+
+ temp = temp->or;
+
+ while ( constraint_isDefined(temp) )
+ {
+ ret = cstring_concatFree (ret, cstring_makeLiteral (" OR ") );
+ ret = cstring_concatFree (ret, constraint_print(temp) );
+ temp = temp->or;
+ }
+
+ return ret;
+
+}
+
/*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
exprNodeList arglist)
{
return postcondition;
}
-constraint constraint_doSRefFixConstraintParam (constraint precondition,
+/*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
exprNodeList arglist)
{
precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
+ precondition->fcnPre = FALSE;
return precondition;
}
// return FALSE;
// }
-/*@only@*/ constraint constraint_preserveOrig (/*@returned@*/ /*@only@*/ constraint c) /*@modifies c @*/
+constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
{
- c->orig = constraint_copy (c);
+
+ DPRINTF( (message("Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
+
+ if (c->orig == constraint_undefined)
+ c->orig = constraint_copy (c);
+
+ else if (c->orig->fcnPre)
+ {
+ constraint temp;
+
+ temp = c->orig;
+
+ /* avoid infinite loop */
+ c->orig = NULL;
+ c->orig = constraint_copy (c);
+ if (c->orig->orig == NULL)
+ {
+ c->orig->orig = temp;
+ temp = NULL;
+ }
+ else
+ {
+ llcontbug((message("Expected c->orig->orig to be null" ) ));
+ constraint_free(c->orig->orig);
+ c->orig->orig = temp;
+ temp = NULL;
+ }
+ }
+ else
+ {
+ DPRINTF( (message("Not changing constraint") ));
+ }
+
+ DPRINTF( (message("After Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
+
return c;
}
/*@=fcnuse*/
/*@=assignexpose*/
/*@=czechfcns@*/
+
+
+constraint constraint_togglePost (/*@returned@*/ constraint c)
+{
+ c->post = !c->post;
+ return c;
+}
+
+constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
+{
+ if (c->orig != NULL)
+ c->orig = constraint_togglePost(c->orig);
+ return c;
+}
+
+bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint c)
+{
+ if (c->orig == NULL)
+ return FALSE;
+ else
+ return TRUE;
+}
+
+
+constraint constraint_undump (FILE *f)
+{
+ constraint c;
+ bool fcnPre;
+ bool post;
+ arithType ar;
+
+ constraintExpr lexpr;
+ constraintExpr expr;
+ // /*@kept@*/ exprNode generatingExpr;
+
+ char * s;
+
+ char *os;
+
+ s = mstring_create (MAX_DUMP_LINE_LENGTH);
+
+ os = s;
+
+ s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+
+ /*@i33*/ /*this should probably be wrappered...*/
+
+ fcnPre = (bool) getInt (&s);
+ advanceField(&s);
+ post = (bool) getInt (&s);
+ advanceField(&s);
+ ar = (arithType) getInt (&s);
+
+ s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+
+ checkChar (&s, 'l');
+
+ lexpr = constraintExpr_undump (f);
+
+ s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+
+ checkChar (&s, 'r');
+ expr = constraintExpr_undump (f);
+
+ c = constraint_makeNew();
+
+ c->fcnPre = fcnPre;
+ c->post = post;
+ c->ar = ar;
+
+ c->lexpr = lexpr;
+ c->expr = expr;
+
+ free(os);
+ return c;
+}
+
+
+void constraint_dump (/*@observer@*/ constraint c, FILE *f)
+{
+ bool fcnPre;
+ bool post;
+ arithType ar;
+
+ constraintExpr lexpr;
+ constraintExpr expr;
+ // /*@kept@*/ exprNode generatingExpr;
+
+ fcnPre = c->fcnPre;
+ post = c->post;
+ ar = c->ar;
+ lexpr = c->lexpr;
+ expr = c->expr;
+
+ fprintf(f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
+ fprintf(f,"l\n");
+ constraintExpr_dump (lexpr, f);
+ fprintf(f,"r\n");
+ constraintExpr_dump (expr, f);
+}
+
+
andersk / splint.git / blobdiff