[splint.git] / src / constraint.c

/*
** constraintList.c
*/

//#define DEBUGPRINT 1

# include <ctype.h> /* for isdigit */
# include "lclintMacros.nf"
# include "basic.h"
# include "cgrammar.h"
# include "cgrammar_tokens.h"

# include "exprChecks.h"
# include "aliasChecks.h"
# include "exprNodeSList.h"
//# include "exprData.i"

/*@i33*/
/*@-fcnuse*/
/*@-assignexpose*/

constraint constraint_makeNew (void);


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

  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("Unsupported relational operator");


  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;
}

constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
     
{
  char *t;
  int c;
  constraint ret;
  ret = constraint_makeNew();
  llassert (l);
  if (!l)
    return ret;
 
    
  ret->lexpr = constraintExpr_copy (l);
  #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("Unsupported relational operator");


  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;
}


constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)     
{
  constraint ret;
  ret = constraint_makeNew();
  llassert (l);
  if (!l)
    return ret;
 
    
  ret->lexpr = constraintExpr_copy (l);
  #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("Unsupported relational operator");

  ret->expr = constraintExpr_copy (r);

  ret->post = TRUE;
  //  ret->orig = ret;
  DPRINTF(("GENERATED CONSTRAINT:"));
  DPRINTF( (message ("%s", constraint_print(ret) ) ) );
  return ret;
}

constraint constraint_copy (constraint c)
{
  constraint ret;
  ret = constraint_makeNew();
  ret->lexpr = constraintExpr_copy (c->lexpr);
  ret->ar = c->ar;
  ret->expr =  constraintExpr_copy (c->expr);
  ret->post = c->post;
  ret->generatingExpr = c->generatingExpr;
  
  /*@i33 fix this*/
  if (c->orig != NULL)
    ret->orig = constraint_copy (c->orig);
  else
    ret->orig = NULL;
  return ret;
}

/*like copy expect it doesn't allocate memory for the constraint*/

void constraint_overWrite (constraint c1, constraint c2)
{
  c1->lexpr = constraintExpr_copy (c2->lexpr);
  c1->ar = c2->ar;
  c1->expr =  constraintExpr_copy (c2->expr);
  c1->post = c2->post;
  /*@i33 fix this*/
  if (c2->orig != NULL)
    c1->orig = constraint_copy (c2->orig);
  else
    c1->orig = NULL;
  c1->generatingExpr = c2->generatingExpr;
}

bool constraint_resolve (/*@unused@*/ constraint c)
{
  return FALSE;
}


constraint constraint_makeNew (void)
{
  constraint ret;
  ret = dmalloc(sizeof (*ret) );
  ret->lexpr = NULL;
  ret->expr = NULL;
  ret->ar = LT;
  ret->post = FALSE;
  ret->orig = NULL;
  ret->generatingExpr = NULL;
  /*@i23*/return ret;
}

constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
{
    
  if (c->generatingExpr == NULL)
    {
      c->generatingExpr = e;
      DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
    }
  else
    {
      DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
    }
  return c;
}

fileloc constraint_getFileloc (constraint c)
{
  if (c->generatingExpr)
    return (exprNode_getfileloc (c->generatingExpr) );
	    
  return (constraintExpr_getFileloc (c->lexpr) );


}

static bool checkForMaxSet (constraint c)
{
  if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
    return TRUE;

  return FALSE;
}

bool constraint_hasMaxSet(constraint c)
{
  if (c->orig)
    {
      if (checkForMaxSet(c->orig) )
	return TRUE;
    }

  return (checkForMaxSet(c) );
}

constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
{
  constraint ret = constraint_makeNew();
  //  constraintTerm term;
  po = exprNode_fakeCopy(po);
  ind = exprNode_fakeCopy(ind);
  ret->lexpr = constraintExpr_makeMaxReadExpr(po);
  ret->ar    = GTE;
  ret->expr  = constraintExpr_makeValueExpr (ind);
  return ret;
}

constraint constraint_makeWriteSafeInt (exprNode po, int ind)
{
  constraint ret = constraint_makeNew();

 
  ret->lexpr =constraintExpr_makeMaxSetExpr(po);
  ret->ar = GTE;
  ret->expr =  constraintExpr_makeValueInt (ind);
  /*@i1*/return ret;
}

constraint constraint_makeSRefSetBufferSize (sRef s, int size)
{
 constraint ret = constraint_makeNew();
 ret->lexpr = constraintExpr_makeSRefMaxset (s);
 ret->ar = EQ;
 ret->expr =  constraintExpr_makeValueInt (size);
 ret->post = TRUE;
 /*@i1*/return ret;
}

constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
{
  constraint ret = constraint_makeNew();

 
  ret->lexpr = constraintExpr_makeSRefMaxset (s);
  ret->ar = GTE;
  ret->expr =  constraintExpr_makeValueInt (ind);
  ret->post = TRUE;
  /*@i1*/return ret;
}

/* drl added 01/12/2000
   
  makes the constraint: Ensures index <= MaxRead(buffer) */

constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
{
  constraint ret = constraint_makeNew();

  ret->lexpr = constraintExpr_makeValueExpr (index);
  ret->ar = LTE;
  ret->expr = constraintExpr_makeMaxReadExpr(buffer);
  ret->post = TRUE;
  return ret;
}

constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
{
  constraint ret = constraint_makeNew();

 
  ret->lexpr =constraintExpr_makeMaxSetExpr(po);
  ret->ar = GTE;
  ret->expr =  constraintExpr_makeValueExpr (ind);
  /*@i1*/return ret;
}


constraint constraint_makeReadSafeInt ( exprNode po, int ind)
{
  constraint ret = constraint_makeNew();

  po = exprNode_fakeCopy(po);
  
  ret->lexpr = constraintExpr_makeMaxReadExpr(po);
  ret->ar    = GTE;
  ret->expr  = constraintExpr_makeValueInt (ind);
  return ret;
}

constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
{
  constraint ret = constraint_makeNew();


  e1 = exprNode_fakeCopy (e1);
  t2 = exprNode_fakeCopy (t2);
  
  ret = constraint_makeReadSafeExprNode(e1, t2);

  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
  
  ret->post = TRUE;  

  //  fileloc_incColumn (ret->lexpr->term->loc);
  return ret;
}


static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint,  arithType  ar)
{
  constraint ret = constraint_makeNew();
  exprNode e;
  
  e = exprNode_fakeCopy(e1);
  if (! (e1 && e2) )
    {
      llcontbug((message("null exprNode, Exprnodes are %s and %s",
		       exprNode_unparse(e1), exprNode_unparse(e2) )
	       ));
    }
		       
  ret->lexpr = constraintExpr_makeValueExpr (e);
  ret->ar = ar;
  ret->post = TRUE;
  e = exprNode_fakeCopy(e2);
  ret->expr =  constraintExpr_makeValueExpr (e);
  
  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
  return ret;
}


/* make constraint ensures e1 == e2 */

constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
{
  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
}

/*make constraint ensures e1 < e2 */
constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
{
 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LT) );
}

constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
{
 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
}

constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
{
 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GT) );
}

constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
{
 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
}


exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
{
  dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
  dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
  dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
  dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
  return dst;
}

constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
{
  constraint ret = constraint_makeNew();
  //constraintTerm term;

  e = exprNode_fakeCopy(e);
  ret->lexpr = constraintExpr_makeValueExpr (e);
  ret->ar = EQ;
  ret->post = TRUE;
  ret->expr =  constraintExpr_makeValueExpr (e);
  ret->expr =  constraintExpr_makeDecConstraintExpr (ret->expr);

  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
//   fileloc_incColumn (  ret->lexpr->term->loc);
//   fileloc_incColumn (  ret->lexpr->term->loc);
  return ret;
}
constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
{
  constraint ret = constraint_makeNew();
  //constraintTerm term;

  e = exprNode_fakeCopy(e);
  ret->lexpr = constraintExpr_makeValueExpr (e);
  ret->ar = EQ;
  ret->post = TRUE;
  ret->expr =  constraintExpr_makeValueExpr (e);
  ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);

  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
//   fileloc_incColumn (  ret->lexpr->term->loc);
//   fileloc_incColumn (  ret->lexpr->term->loc);
  return ret;
}


// constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
// {
//   constraint ret = constraint_makeNew();
//   //constraintTerm term;

//   e = exprNode_fakeCopy(e);
//   ret->lexpr = constraintExpr_makeMaxReadExpr(e);
//   ret->ar = EQ;
//   ret->post = TRUE;
//   ret->expr = constraintExpr_makeIncConstraintExpr (e);
//   ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
//   return ret;
// }


cstring arithType_print (arithType ar)
{
  cstring st = cstring_undefined;
  switch (ar)
    {
    case LT:
      st = cstring_makeLiteral (" < ");
      break;
    case	LTE:
      st = cstring_makeLiteral (" <= ");
      break;
    case 	GT:
      st = cstring_makeLiteral (" > ");
      break;
    case 	GTE:
      st = cstring_makeLiteral (" >= ");
      break;
    case	EQ:
      st = cstring_makeLiteral (" == ");
      break;
    case	NONNEGATIVE:
      st = cstring_makeLiteral (" NONNEGATIVE ");
      break;
    case	POSITIVE:
      st = cstring_makeLiteral (" POSITIVE ");
      break;
    default:
      llassert(FALSE);
      break;
    }
  return st;
}

void constraint_printError (constraint c, fileloc loc)
{
  cstring string;
  fileloc errorLoc;
  
  string = constraint_printDetailed (c);

  errorLoc = loc;

  if (constraint_getFileloc(c) )
    errorLoc = constraint_getFileloc(c);
  
  
  if (c->post)
    {
       voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
    }
  else
    {
      voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
    }
      
}

cstring  constraint_printDetailed (constraint c)
{
  cstring st = cstring_undefined;


  if (!c->post)
    {
    if (c->orig)  
      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));
      
    }
  else
    {
      if (c->orig)
	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));	
    }

  if (context_getFlag (FLG_CONSTRAINTLOCATION) )
    {
      cstring temp;
      // llassert (c->generatingExpr);
      temp = message ("\nOriginal Generating expression %s: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
		      exprNode_unparse(c->generatingExpr) );
      st = cstring_concat (st, temp);

      if (constraint_hasMaxSet(c) )
	{
	  cstring temp2;
	  temp2 = message ("\nHas MaxSet\n");
	  st = cstring_concat (st, temp2);
	}
    }
  return st;
}

cstring  constraint_print (constraint c) /*@*/
{
  cstring st = cstring_undefined;
  cstring type = cstring_undefined;
  llassert (c);
  if (c->post)
    {
      type = cstring_makeLiteral ("Ensures: ");
    }
  else
    {
      type = cstring_makeLiteral ("Requires: ");
    }
  st = message ("%s: %s %s %s",
		type,
		constraintExpr_print (c->lexpr),
		arithType_print(c->ar),
		constraintExpr_print(c->expr)
		);
  return st;
}

constraint constraint_doSRefFixBaseParam (constraint precondition,
						   exprNodeList arglist)
{
  precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
							   arglist);
  precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
							   arglist);

  return precondition;
}


constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
{
  postcondition = constraint_copy (postcondition);
  postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
  postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);

  return postcondition;
}

constraint constraint_doSRefFixConstraintParam (constraint precondition,
						   exprNodeList arglist)
{

  precondition = constraint_copy (precondition);
  precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
  precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);

  return precondition;
}

// bool constraint_hasTerm (constraint c, constraintTerm term)
// {
//   DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
  
//   if (constraintExpr_includesTerm (c->lexpr, term) )
//     return TRUE;

//   if (constraintExpr_includesTerm (c->expr, term) )
//     return TRUE;

//   return FALSE;
// }

constraint constraint_preserveOrig (constraint c)
{
  c->orig = constraint_copy (c);
  return c;
}
/*@=fcnuse*/
/*@=assignexpose*/
/*@=czechfcns@*/
Commit	Line	Data
616915dd	1	/*
	2	** constraintList.c
	3	*/
	4
	5	//#define DEBUGPRINT 1
	6
	7	# include <ctype.h> /* for isdigit */
	8	# include "lclintMacros.nf"
	9	# include "basic.h"
	10	# include "cgrammar.h"
	11	# include "cgrammar_tokens.h"
	12
	13	# include "exprChecks.h"
	14	# include "aliasChecks.h"
	15	# include "exprNodeSList.h"
	16	//# include "exprData.i"
	17
	18	/@i33/
	19	/@-fcnuse/
	20	/@-assignexpose/
	21
	22	constraint constraint_makeNew (void);
	23
	24
	25	constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant)
	26
	27	{
	28	char *t;
	29	int c;
	30	constraint ret;
	31	ret = constraint_makeNew();
	32	llassert (sRef_isValid(x) );
	33	if (!sRef_isValid(x))
	34	return ret;
	35
	36
	37	ret->lexpr = constraintExpr_makeTermsRef (x);
	38	#warning fix abstraction
	39
	40	if (relOp.tok == GE_OP)
	41	ret->ar = GTE;
	42	else if (relOp.tok == LE_OP)
	43	ret->ar = LTE;
	44	else if (relOp.tok == EQ_OP)
	45	ret->ar = EQ;
	46	else
	47	llfatalbug("Unsupported relational operator");
	48
	49
	50	t = cstring_toCharsSafe (exprNode_unparse(cconstant));
	51	c = atoi( t );
	52	ret->expr = constraintExpr_makeIntLiteral (c);
	53
	54	ret->post = TRUE;
	55	// ret->orig = ret;
	56	DPRINTF(("GENERATED CONSTRAINT:"));
	57	DPRINTF( (message ("%s", constraint_print(ret) ) ) );
	58	return ret;
	59	}
	60
	61	constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
	62
	63	{
	64	char *t;
65	int c;
66	constraint ret;
67	ret = constraint_makeNew();
68	llassert (l);
69	if (!l)
70	return ret;
71
72
73	ret->lexpr = constraintExpr_copy (l);
74	#warning fix abstraction
75
76	if (relOp.tok == GE_OP)
77	ret->ar = GTE;
78	else if (relOp.tok == LE_OP)
79	ret->ar = LTE;
80	else if (relOp.tok == EQ_OP)
81	ret->ar = EQ;
82	else
83	llfatalbug("Unsupported relational operator");
84
85
86	t = cstring_toCharsSafe (exprNode_unparse(cconstant));
87	c = atoi( t );
88	ret->expr = constraintExpr_makeIntLiteral (c);
89
90	ret->post = TRUE;
91	// ret->orig = ret;
92	DPRINTF(("GENERATED CONSTRAINT:"));
93	DPRINTF( (message ("%s", constraint_print(ret) ) ) );
94	return ret;
95	}
96
97
98	constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
99	{
100	constraint ret;
101	ret = constraint_makeNew();
102	llassert (l);
103	if (!l)
104	return ret;
105
106
107	ret->lexpr = constraintExpr_copy (l);
108	#warning fix abstraction
109
110	if (relOp.tok == GE_OP)
111	ret->ar = GTE;
112	else if (relOp.tok == LE_OP)
113	ret->ar = LTE;
114	else if (relOp.tok == EQ_OP)
115	ret->ar = EQ;
116	else
117	llfatalbug("Unsupported relational operator");
118
119	ret->expr = constraintExpr_copy (r);
120
121	ret->post = TRUE;
122	// ret->orig = ret;
123	DPRINTF(("GENERATED CONSTRAINT:"));
124	DPRINTF( (message ("%s", constraint_print(ret) ) ) );
125	return ret;
126	}
127
128	constraint constraint_copy (constraint c)
129	{
130	constraint ret;
131	ret = constraint_makeNew();
132	ret->lexpr = constraintExpr_copy (c->lexpr);
133	ret->ar = c->ar;
134	ret->expr = constraintExpr_copy (c->expr);
135	ret->post = c->post;
9280addf	136	ret->generatingExpr = c->generatingExpr;
9280addf	137
616915dd	138	/@i33 fix this/
	139	if (c->orig != NULL)
	140	ret->orig = constraint_copy (c->orig);
	141	else
	142	ret->orig = NULL;
	143	return ret;
	144	}
	145
	146	/like copy expect it doesn't allocate memory for the constraint/
	147
	148	void constraint_overWrite (constraint c1, constraint c2)
	149	{
	150	c1->lexpr = constraintExpr_copy (c2->lexpr);
	151	c1->ar = c2->ar;
	152	c1->expr = constraintExpr_copy (c2->expr);
	153	c1->post = c2->post;
	154	/@i33 fix this/
	155	if (c2->orig != NULL)
	156	c1->orig = constraint_copy (c2->orig);
	157	else
	158	c1->orig = NULL;
9280addf	159	c1->generatingExpr = c2->generatingExpr;
616915dd	160	}
	161
	162	bool constraint_resolve (/@unused@/ constraint c)
	163	{
	164	return FALSE;
	165	}
	166
	167
	168
	169	constraint constraint_makeNew (void)
	170	{
	171	constraint ret;
	172	ret = dmalloc(sizeof (*ret) );
	173	ret->lexpr = NULL;
	174	ret->expr = NULL;
	175	ret->ar = LT;
	176	ret->post = FALSE;
	177	ret->orig = NULL;
9280addf	178	ret->generatingExpr = NULL;
616915dd	179	/@i23/return ret;
	180	}
	181
9280addf	182	constraint constraint_addGeneratingExpr (/@returned@/ constraint c, exprNode e)
	183	{
	184
	185	if (c->generatingExpr == NULL)
	186	{
	187	c->generatingExpr = e;
	188	DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
	189	}
	190	else
	191	{
	192	DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
	193	}
	194	return c;
	195	}
	196
616915dd	197	fileloc constraint_getFileloc (constraint c)
616915dd	198	{
9280addf	199	if (c->generatingExpr)
	200	return (exprNode_getfileloc (c->generatingExpr) );
	201
616915dd	202	return (constraintExpr_getFileloc (c->lexpr) );
	203
	204
	205	}
	206
9280addf	207	static bool checkForMaxSet (constraint c)
	208	{
	209	if (constraintExpr_hasMaxSet(c->lexpr) \|\| constraintExpr_hasMaxSet(c->expr) )
	210	return TRUE;
	211
	212	return FALSE;
	213	}
	214
	215	bool constraint_hasMaxSet(constraint c)
	216	{
	217	if (c->orig)
	218	{
	219	if (checkForMaxSet(c->orig) )
	220	return TRUE;
	221	}
	222
	223	return (checkForMaxSet(c) );
	224	}
	225
616915dd	226	constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
	227	{
	228	constraint ret = constraint_makeNew();
	229	// constraintTerm term;
	230	po = exprNode_fakeCopy(po);
	231	ind = exprNode_fakeCopy(ind);
	232	ret->lexpr = constraintExpr_makeMaxReadExpr(po);
	233	ret->ar = GTE;
	234	ret->expr = constraintExpr_makeValueExpr (ind);
	235	return ret;
	236	}
	237
	238	constraint constraint_makeWriteSafeInt (exprNode po, int ind)
	239	{
	240	constraint ret = constraint_makeNew();
	241
	242
	243	ret->lexpr =constraintExpr_makeMaxSetExpr(po);
	244	ret->ar = GTE;
	245	ret->expr = constraintExpr_makeValueInt (ind);
	246	/@i1/return ret;
	247	}
	248
	249	constraint constraint_makeSRefSetBufferSize (sRef s, int size)
	250	{
	251	constraint ret = constraint_makeNew();
	252	ret->lexpr = constraintExpr_makeSRefMaxset (s);
	253	ret->ar = EQ;
	254	ret->expr = constraintExpr_makeValueInt (size);
	255	ret->post = TRUE;
	256	/@i1/return ret;
	257	}
	258
	259	constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
	260	{
	261	constraint ret = constraint_makeNew();
	262
	263
	264	ret->lexpr = constraintExpr_makeSRefMaxset (s);
	265	ret->ar = GTE;
	266	ret->expr = constraintExpr_makeValueInt (ind);
	267	ret->post = TRUE;
	268	/@i1/return ret;
	269	}
	270
	271	/* drl added 01/12/2000
	272
	273	makes the constraint: Ensures index <= MaxRead(buffer) */
	274
	275	constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
	276	{
	277	constraint ret = constraint_makeNew();
	278
	279	ret->lexpr = constraintExpr_makeValueExpr (index);
	280	ret->ar = LTE;
	281	ret->expr = constraintExpr_makeMaxReadExpr(buffer);
	282	ret->post = TRUE;
	283	return ret;
	284	}
	285
	286	constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
	287	{
	288	constraint ret = constraint_makeNew();
	289
290
291	ret->lexpr =constraintExpr_makeMaxSetExpr(po);
292	ret->ar = GTE;
293	ret->expr = constraintExpr_makeValueExpr (ind);
294	/@i1/return ret;
295	}
296
297
298	constraint constraint_makeReadSafeInt ( exprNode po, int ind)
299	{
300	constraint ret = constraint_makeNew();
301
302	po = exprNode_fakeCopy(po);
303
304	ret->lexpr = constraintExpr_makeMaxReadExpr(po);
305	ret->ar = GTE;
306	ret->expr = constraintExpr_makeValueInt (ind);
307	return ret;
308	}
309
310	constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
311	{
312	constraint ret = constraint_makeNew();
313
314
315	e1 = exprNode_fakeCopy (e1);
316	t2 = exprNode_fakeCopy (t2);
317
318	ret = constraint_makeReadSafeExprNode(e1, t2);
319
320	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
321
322	ret->post = TRUE;
323
324	// fileloc_incColumn (ret->lexpr->term->loc);
325	return ret;
326	}
327
328
329	static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint, arithType ar)
330	{
331	constraint ret = constraint_makeNew();
332	exprNode e;
333
334	e = exprNode_fakeCopy(e1);
335	if (! (e1 && e2) )
336	{
337	llcontbug((message("null exprNode, Exprnodes are %s and %s",
338	exprNode_unparse(e1), exprNode_unparse(e2) )
339	));
340	}
341
342	ret->lexpr = constraintExpr_makeValueExpr (e);
343	ret->ar = ar;
344	ret->post = TRUE;
345	e = exprNode_fakeCopy(e2);
346	ret->expr = constraintExpr_makeValueExpr (e);
347
348	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
349	return ret;
350	}
351
352
353	/* make constraint ensures e1 == e2 */
354
355	constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
356	{
357	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
358	}
359
360	/make constraint ensures e1 < e2 /
361	constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
362	{
363	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LT) );
364	}
365
366	constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
367	{
368	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
369	}
370
371	constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
372	{
373	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GT) );
374	}
375
376	constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
377	{
378	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
379	}
380
381
382	exprNode exprNode_copyConstraints (/@returned@/ exprNode dst, exprNode src)
383	{
384	dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
385	dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
386	dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
387	dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
388	return dst;
389	}
390
391	constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
392	{
393	constraint ret = constraint_makeNew();
394	//constraintTerm term;
395
396	e = exprNode_fakeCopy(e);
397	ret->lexpr = constraintExpr_makeValueExpr (e);
398	ret->ar = EQ;
399	ret->post = TRUE;
400	ret->expr = constraintExpr_makeValueExpr (e);
401	ret->expr = constraintExpr_makeDecConstraintExpr (ret->expr);
402
403	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
404	// fileloc_incColumn ( ret->lexpr->term->loc);
405	// fileloc_incColumn ( ret->lexpr->term->loc);
406	return ret;
407	}
408	constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
409	{
410	constraint ret = constraint_makeNew();
411	//constraintTerm term;
412
413	e = exprNode_fakeCopy(e);
414	ret->lexpr = constraintExpr_makeValueExpr (e);
415	ret->ar = EQ;
416	ret->post = TRUE;
417	ret->expr = constraintExpr_makeValueExpr (e);
418	ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
419
420	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
421	// fileloc_incColumn ( ret->lexpr->term->loc);
422	// fileloc_incColumn ( ret->lexpr->term->loc);
423	return ret;
424	}
425
426
427
428	// constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
429	// {
430	// constraint ret = constraint_makeNew();
431	// //constraintTerm term;
432
433	// e = exprNode_fakeCopy(e);
434	// ret->lexpr = constraintExpr_makeMaxReadExpr(e);
435	// ret->ar = EQ;
436	// ret->post = TRUE;
437	// ret->expr = constraintExpr_makeIncConstraintExpr (e);
438	// ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
439	// return ret;
440	// }
441
442
443	cstring arithType_print (arithType ar)
444	{
445	cstring st = cstring_undefined;
446	switch (ar)
447	{
448	case LT:
449	st = cstring_makeLiteral (" < ");
450	break;
451	case LTE:
452	st = cstring_makeLiteral (" <= ");
453	break;
454	case GT:
455	st = cstring_makeLiteral (" > ");
456	break;
457	case GTE:
458	st = cstring_makeLiteral (" >= ");
459	break;
460	case EQ:
461	st = cstring_makeLiteral (" == ");
462	break;
463	case NONNEGATIVE:
464	st = cstring_makeLiteral (" NONNEGATIVE ");
465	break;
466	case POSITIVE:
467	st = cstring_makeLiteral (" POSITIVE ");
468	break;
469	default:
470	llassert(FALSE);
471	break;
472	}
473	return st;
474	}
475
476	void constraint_printError (constraint c, fileloc loc)
477	{
478	cstring string;
9280addf	479	fileloc errorLoc;
9280addf	480
616915dd	481	string = constraint_printDetailed (c);
9280addf	482
	483	errorLoc = loc;
	484
	485	if (constraint_getFileloc(c) )
	486	errorLoc = constraint_getFileloc(c);
	487
616915dd	488
	489	if (c->post)
	490	{
9280addf	491	voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
616915dd	492	}
	493	else
	494	{
9280addf	495	voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
616915dd	496	}
	497
	498	}
	499
	500	cstring constraint_printDetailed (constraint c)
	501	{
	502	cstring st = cstring_undefined;
	503
	504
	505	if (!c->post)
	506	{
	507	if (c->orig)
	508	st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisfy %s", constraint_print (c), constraint_print(c->orig) );
	509	else
	510	st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
	511
	512	}
	513	else
	514	{
	515	if (c->orig)
	516	st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
	517	else
	518	st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));
	519	}
9280addf	520
	521	if (context_getFlag (FLG_CONSTRAINTLOCATION) )
	522	{
	523	cstring temp;
	524	// llassert (c->generatingExpr);
	525	temp = message ("\nOriginal Generating expression %s: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
	526	exprNode_unparse(c->generatingExpr) );
	527	st = cstring_concat (st, temp);
	528
	529	if (constraint_hasMaxSet(c) )
	530	{
	531	cstring temp2;
	532	temp2 = message ("\nHas MaxSet\n");
	533	st = cstring_concat (st, temp2);
	534	}
	535	}
616915dd	536	return st;
	537	}
	538
	539	cstring constraint_print (constraint c) /@/
	540	{
	541	cstring st = cstring_undefined;
	542	cstring type = cstring_undefined;
	543	llassert (c);
	544	if (c->post)
	545	{
	546	type = cstring_makeLiteral ("Ensures: ");
	547	}
	548	else
	549	{
	550	type = cstring_makeLiteral ("Requires: ");
	551	}
	552	st = message ("%s: %s %s %s",
	553	type,
	554	constraintExpr_print (c->lexpr),
	555	arithType_print(c->ar),
	556	constraintExpr_print(c->expr)
	557	);
	558	return st;
	559	}
	560
	561	constraint constraint_doSRefFixBaseParam (constraint precondition,
	562	exprNodeList arglist)
	563	{
	564	precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
	565	arglist);
	566	precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
	567	arglist);
	568
	569	return precondition;
	570	}
	571
	572
	573	constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
	574	{
	575	postcondition = constraint_copy (postcondition);
	576	postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
	577	postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
	578
	579	return postcondition;
	580	}
	581
	582	constraint constraint_doSRefFixConstraintParam (constraint precondition,
	583	exprNodeList arglist)
	584	{
	585
	586	precondition = constraint_copy (precondition);
	587	precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
	588	precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
	589
	590	return precondition;
	591	}
	592
	593	// bool constraint_hasTerm (constraint c, constraintTerm term)
	594	// {
	595	// DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
	596
	597	// if (constraintExpr_includesTerm (c->lexpr, term) )
	598	// return TRUE;
	599
600	// if (constraintExpr_includesTerm (c->expr, term) )
601	// return TRUE;
602
603	// return FALSE;
604	// }
605
606	constraint constraint_preserveOrig (constraint c)
607	{
608	c->orig = constraint_copy (c);
609	return c;
610	}
611	/@=fcnuse/
612	/@=assignexpose/
613	/@=czechfcns@/