[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;
  /*@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;

}

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;
  /*@i23*/return ret;
}

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


}

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


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) )
    {
      TPRINTF((message("Warning 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 (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_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;

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

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 satisy %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));	
    }
  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;
}


// 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
4cccc6ad	1	/*
	2	** constraintList.c
	3	*/
	4
f5ac53de	5	//#define DEBUGPRINT 1
f5ac53de	6
4cccc6ad	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"
93307a76	16	//# include "exprData.i"
4cccc6ad	17
	18	/@i33/
	19	/@-fcnuse/
	20	/@-assignexpose/
	21
93307a76	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();
f5ac53de	32	llassert (sRef_isValid(x) );
f5ac53de	33	if (!sRef_isValid(x))
93307a76	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	}
361091cc	127
4cccc6ad	128	constraint constraint_copy (constraint c)
	129	{
	130	constraint ret;
	131	ret = constraint_makeNew();
bf92e32c	132	ret->lexpr = constraintExpr_copy (c->lexpr);
4cccc6ad	133	ret->ar = c->ar;
bf92e32c	134	ret->expr = constraintExpr_copy (c->expr);
4cccc6ad	135	ret->post = c->post;
bf92e32c	136	/@i33 fix this/
	137	if (c->orig != NULL)
	138	ret->orig = constraint_copy (c->orig);
	139	else
	140	ret->orig = NULL;
4cccc6ad	141	return ret;
	142	}
	143
92c4a786	144	/like copy expect it doesn't allocate memory for the constraint/
	145
	146	void constraint_overWrite (constraint c1, constraint c2)
	147	{
	148	c1->lexpr = constraintExpr_copy (c2->lexpr);
	149	c1->ar = c2->ar;
	150	c1->expr = constraintExpr_copy (c2->expr);
	151	c1->post = c2->post;
	152	/@i33 fix this/
	153	if (c2->orig != NULL)
	154	c1->orig = constraint_copy (c2->orig);
	155	else
	156	c1->orig = NULL;
	157
	158	}
	159
4cccc6ad	160	bool constraint_resolve (/@unused@/ constraint c)
	161	{
	162	return FALSE;
	163	}
	164
93307a76	165
	166
	167	constraint constraint_makeNew (void)
4cccc6ad	168	{
	169	constraint ret;
	170	ret = dmalloc(sizeof (*ret) );
361091cc	171	ret->lexpr = NULL;
361091cc	172	ret->expr = NULL;
4cccc6ad	173	ret->ar = LT;
4cccc6ad	174	ret->post = FALSE;
bf92e32c	175	ret->orig = NULL;
4cccc6ad	176	/@i23/return ret;
4cccc6ad	177	}
4cccc6ad	178
92c4a786	179	fileloc constraint_getFileloc (constraint c)
361091cc	180	{
92c4a786	181	return (constraintExpr_getFileloc (c->lexpr) );
4cccc6ad	182
4cccc6ad	183
4cccc6ad	184	}
4cccc6ad	185
361091cc	186	constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
	187	{
	188	constraint ret = constraint_makeNew();
	189	// constraintTerm term;
	190	po = exprNode_fakeCopy(po);
	191	ind = exprNode_fakeCopy(ind);
	192	ret->lexpr = constraintExpr_makeMaxReadExpr(po);
	193	ret->ar = GTE;
	194	ret->expr = constraintExpr_makeValueExpr (ind);
	195	return ret;
	196	}
4cccc6ad	197
361091cc	198	constraint constraint_makeWriteSafeInt (exprNode po, int ind)
4cccc6ad	199	{
4cccc6ad	200	constraint ret = constraint_makeNew();
92c4a786	201
361091cc	202
361091cc	203	ret->lexpr =constraintExpr_makeMaxSetExpr(po);
4cccc6ad	204	ret->ar = GTE;
361091cc	205	ret->expr = constraintExpr_makeValueInt (ind);
361091cc	206	/@i1/return ret;
4cccc6ad	207	}
34f0c5e7	208
	209
	210	constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
	211	{
	212	constraint ret = constraint_makeNew();
	213
	214
	215	ret->lexpr = constraintExpr_makeSRefMaxset (s);
	216	ret->ar = GTE;
	217	ret->expr = constraintExpr_makeValueInt (ind);
	218	ret->post = TRUE;
	219	/@i1/return ret;
	220	}
	221
	222
92c4a786	223	constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
	224	{
	225	constraint ret = constraint_makeNew();
	226
	227
	228	ret->lexpr =constraintExpr_makeMaxSetExpr(po);
	229	ret->ar = GTE;
	230	ret->expr = constraintExpr_makeValueExpr (ind);
	231	/@i1/return ret;
	232	}
34f0c5e7	233
34f0c5e7	234
361091cc	235	constraint constraint_makeReadSafeInt ( exprNode po, int ind)
	236	{
	237	constraint ret = constraint_makeNew();
4cccc6ad	238
361091cc	239	po = exprNode_fakeCopy(po);
	240
	241	ret->lexpr = constraintExpr_makeMaxReadExpr(po);
	242	ret->ar = GTE;
	243	ret->expr = constraintExpr_makeValueInt (ind);
	244	return ret;
	245	}
4cccc6ad	246
361091cc	247	constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
4cccc6ad	248	{
4cccc6ad	249	constraint ret = constraint_makeNew();
92c4a786	250
4cccc6ad	251
361091cc	252	e1 = exprNode_fakeCopy (e1);
4cccc6ad	253	t2 = exprNode_fakeCopy (t2);
4cccc6ad	254
361091cc	255	ret = constraint_makeReadSafeExprNode(e1, t2);
92c4a786	256
92c4a786	257	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
4cccc6ad	258
4cccc6ad	259	ret->post = TRUE;
361091cc	260
92c4a786	261	// fileloc_incColumn (ret->lexpr->term->loc);
361091cc	262	return ret;
4cccc6ad	263	}
4cccc6ad	264
361091cc	265
34f0c5e7	266	static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint, arithType ar)
754746a0	267	{
	268	constraint ret = constraint_makeNew();
	269	exprNode e;
	270
	271	e = exprNode_fakeCopy(e1);
d8b37170	272	if (! (e1 && e2) )
	273	{
	274	TPRINTF((message("Warning null exprNode, Exprnodes are %s and %s",
	275	exprNode_unparse(e1), exprNode_unparse(e2) )
	276	));
	277	}
	278
754746a0	279	ret->lexpr = constraintExpr_makeValueExpr (e);
34f0c5e7	280	ret->ar = ar;
754746a0	281	ret->post = TRUE;
	282	e = exprNode_fakeCopy(e2);
	283	ret->expr = constraintExpr_makeValueExpr (e);
	284
	285	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
754746a0	286	return ret;
	287	}
	288
	289
34f0c5e7	290	/* make constraint ensures e1 == e2 */
	291
	292	constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
	293	{
	294	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
	295	}
	296
	297	/make constraint ensures e1 < e2 /
	298	constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
	299	{
	300	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LT) );
	301	}
	302
	303	constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
	304	{
	305	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
	306	}
	307
	308	constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
	309	{
	310	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GT) );
	311	}
	312
	313	constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
	314	{
	315	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
	316	}
	317
	318
754746a0	319	exprNode exprNode_copyConstraints (exprNode dst, exprNode src)
	320	{
	321	dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
	322	dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
	323	dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
	324	dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
	325	return dst;
	326	}
	327
361091cc	328	constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
4cccc6ad	329	{
	330	constraint ret = constraint_makeNew();
	331	//constraintTerm term;
92c4a786	332
361091cc	333	e = exprNode_fakeCopy(e);
bf92e32c	334	ret->lexpr = constraintExpr_makeValueExpr (e);
4cccc6ad	335	ret->ar = EQ;
4cccc6ad	336	ret->post = TRUE;
92c4a786	337	ret->expr = constraintExpr_makeValueExpr (e);
92c4a786	338	ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
4cccc6ad	339
754746a0	340	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
92c4a786	341	// fileloc_incColumn ( ret->lexpr->term->loc);
92c4a786	342	// fileloc_incColumn ( ret->lexpr->term->loc);
361091cc	343	return ret;
4cccc6ad	344	}
361091cc	345
754746a0	346
754746a0	347
92c4a786	348	// constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
	349	// {
	350	// constraint ret = constraint_makeNew();
	351	// //constraintTerm term;
4cccc6ad	352
92c4a786	353	// e = exprNode_fakeCopy(e);
	354	// ret->lexpr = constraintExpr_makeMaxReadExpr(e);
	355	// ret->ar = EQ;
	356	// ret->post = TRUE;
	357	// ret->expr = constraintExpr_makeIncConstraintExpr (e);
	358	// ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
	359	// return ret;
	360	// }
4cccc6ad	361
361091cc	362
361091cc	363	cstring arithType_print (arithType ar)
4cccc6ad	364	{
361091cc	365	cstring st = cstring_undefined;
4cccc6ad	366	switch (ar)
	367	{
	368	case LT:
361091cc	369	st = cstring_makeLiteral (" < ");
361091cc	370	break;
4cccc6ad	371	case LTE:
361091cc	372	st = cstring_makeLiteral (" <= ");
361091cc	373	break;
4cccc6ad	374	case GT:
361091cc	375	st = cstring_makeLiteral (" > ");
361091cc	376	break;
4cccc6ad	377	case GTE:
361091cc	378	st = cstring_makeLiteral (" >= ");
361091cc	379	break;
4cccc6ad	380	case EQ:
361091cc	381	st = cstring_makeLiteral (" == ");
361091cc	382	break;
4cccc6ad	383	case NONNEGATIVE:
361091cc	384	st = cstring_makeLiteral (" NONNEGATIVE ");
361091cc	385	break;
4cccc6ad	386	case POSITIVE:
361091cc	387	st = cstring_makeLiteral (" POSITIVE ");
361091cc	388	break;
4cccc6ad	389	default:
4cccc6ad	390	llassert(FALSE);
361091cc	391	break;
4cccc6ad	392	}
361091cc	393	return st;
4cccc6ad	394	}
4cccc6ad	395
f5ac53de	396	void constraint_printError (constraint c, fileloc loc)
	397	{
	398	cstring string;
	399
	400	string = constraint_printDetailed (c);
	401
	402	if (c->post)
	403	{
	404	voptgenerror (FLG_FUNCTIONPOST, string, loc);
	405	}
	406	else
	407	{
	408	voptgenerror (FLG_FUNCTIONCONSTRAINT, string, loc);
	409	}
	410
	411	}
4cccc6ad	412
bf92e32c	413	cstring constraint_printDetailed (constraint c)
	414	{
	415	cstring st = cstring_undefined;
	416
f5ac53de	417
bf92e32c	418	if (!c->post)
bf92e32c	419	{
93307a76	420	if (c->orig)
	421	st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisy %s", constraint_print (c), constraint_print(c->orig) );
	422	else
	423	st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
bf92e32c	424
bf92e32c	425	}
	426	else
	427	{
93307a76	428	if (c->orig)
	429	st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
	430	else
	431	st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));
bf92e32c	432	}
	433	return st;
	434	}
	435
f5ac53de	436	cstring constraint_print (constraint c) /@/
4cccc6ad	437	{
361091cc	438	cstring st = cstring_undefined;
	439	cstring type = cstring_undefined;
	440	llassert (c);
4cccc6ad	441	if (c->post)
4cccc6ad	442	{
361091cc	443	type = cstring_makeLiteral ("Ensures: ");
4cccc6ad	444	}
	445	else
	446	{
361091cc	447	type = cstring_makeLiteral ("Requires: ");
4cccc6ad	448	}
361091cc	449	st = message ("%s: %s %s %s",
	450	type,
	451	constraintExpr_print (c->lexpr),
	452	arithType_print(c->ar),
	453	constraintExpr_print(c->expr)
	454	);
	455	return st;
4cccc6ad	456	}
4cccc6ad	457
93307a76	458	constraint constraint_doSRefFixBaseParam (constraint precondition,
	459	exprNodeList arglist)
	460	{
	461	precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
	462	arglist);
	463	precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
	464	arglist);
	465
	466	return precondition;
	467	}
	468
	469
92c4a786	470	// bool constraint_hasTerm (constraint c, constraintTerm term)
	471	// {
	472	// DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
bf92e32c	473
92c4a786	474	// if (constraintExpr_includesTerm (c->lexpr, term) )
92c4a786	475	// return TRUE;
bf92e32c	476
92c4a786	477	// if (constraintExpr_includesTerm (c->expr, term) )
92c4a786	478	// return TRUE;
bf92e32c	479
92c4a786	480	// return FALSE;
92c4a786	481	// }
bf92e32c	482
	483	constraint constraint_preserveOrig (constraint c)
	484	{
	485	c->orig = constraint_copy (c);
	486	return c;
	487	}
4cccc6ad	488	/@=fcnuse/
	489	/@=assignexpose/
	490	/@=czechfcns@/