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

  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 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));	
    }
  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;
136	/@i33 fix this/
137	if (c->orig != NULL)
138	ret->orig = constraint_copy (c->orig);
139	else
140	ret->orig = NULL;
141	return ret;
142	}
143
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
160	bool constraint_resolve (/@unused@/ constraint c)
161	{
162	return FALSE;
163	}
164
165
166
167	constraint constraint_makeNew (void)
168	{
169	constraint ret;
170	ret = dmalloc(sizeof (*ret) );
171	ret->lexpr = NULL;
172	ret->expr = NULL;
173	ret->ar = LT;
174	ret->post = FALSE;
175	ret->orig = NULL;
176	/@i23/return ret;
177	}
178
179	fileloc constraint_getFileloc (constraint c)
180	{
181	return (constraintExpr_getFileloc (c->lexpr) );
182
183
184	}
185
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	}
197
198	constraint constraint_makeWriteSafeInt (exprNode po, int ind)
199	{
200	constraint ret = constraint_makeNew();
201
202
203	ret->lexpr =constraintExpr_makeMaxSetExpr(po);
204	ret->ar = GTE;
205	ret->expr = constraintExpr_makeValueInt (ind);
206	/@i1/return ret;
207	}
208
209	constraint constraint_makeSRefSetBufferSize (sRef s, int size)
210	{
211	constraint ret = constraint_makeNew();
212	ret->lexpr = constraintExpr_makeSRefMaxset (s);
213	ret->ar = EQ;
214	ret->expr = constraintExpr_makeValueInt (size);
215	ret->post = TRUE;
216	/@i1/return ret;
217	}
218
219	constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
220	{
221	constraint ret = constraint_makeNew();
222
223
224	ret->lexpr = constraintExpr_makeSRefMaxset (s);
225	ret->ar = GTE;
226	ret->expr = constraintExpr_makeValueInt (ind);
227	ret->post = TRUE;
228	/@i1/return ret;
229	}
230
231	/* drl added 01/12/2000
232
233	makes the constraint: Ensures index <= MaxRead(buffer) */
234
235	constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
236	{
237	constraint ret = constraint_makeNew();
238
239	ret->lexpr = constraintExpr_makeValueExpr (index);
240	ret->ar = LTE;
241	ret->expr = constraintExpr_makeMaxReadExpr(buffer);
242	ret->post = TRUE;
243	return ret;
244	}
245
246	constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
247	{
248	constraint ret = constraint_makeNew();
249
250
251	ret->lexpr =constraintExpr_makeMaxSetExpr(po);
252	ret->ar = GTE;
253	ret->expr = constraintExpr_makeValueExpr (ind);
254	/@i1/return ret;
255	}
256
257
258	constraint constraint_makeReadSafeInt ( exprNode po, int ind)
259	{
260	constraint ret = constraint_makeNew();
261
262	po = exprNode_fakeCopy(po);
263
264	ret->lexpr = constraintExpr_makeMaxReadExpr(po);
265	ret->ar = GTE;
266	ret->expr = constraintExpr_makeValueInt (ind);
267	return ret;
268	}
269
270	constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
271	{
272	constraint ret = constraint_makeNew();
273
274
275	e1 = exprNode_fakeCopy (e1);
276	t2 = exprNode_fakeCopy (t2);
277
278	ret = constraint_makeReadSafeExprNode(e1, t2);
279
280	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
281
282	ret->post = TRUE;
283
284	// fileloc_incColumn (ret->lexpr->term->loc);
285	return ret;
286	}
287
288
289	static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint, arithType ar)
290	{
291	constraint ret = constraint_makeNew();
292	exprNode e;
293
294	e = exprNode_fakeCopy(e1);
295	if (! (e1 && e2) )
296	{
297	llcontbug((message("null exprNode, Exprnodes are %s and %s",
298	exprNode_unparse(e1), exprNode_unparse(e2) )
299	));
300	}
301
302	ret->lexpr = constraintExpr_makeValueExpr (e);
303	ret->ar = ar;
304	ret->post = TRUE;
305	e = exprNode_fakeCopy(e2);
306	ret->expr = constraintExpr_makeValueExpr (e);
307
308	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
309	return ret;
310	}
311
312
313	/* make constraint ensures e1 == e2 */
314
315	constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
316	{
317	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
318	}
319
320	/make constraint ensures e1 < e2 /
321	constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
322	{
323	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LT) );
324	}
325
326	constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
327	{
328	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
329	}
330
331	constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
332	{
333	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GT) );
334	}
335
336	constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
337	{
338	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
339	}
340
341
342	exprNode exprNode_copyConstraints (/@returned@/ exprNode dst, exprNode src)
343	{
344	dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
345	dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
346	dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
347	dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
348	return dst;
349	}
350
351	constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
352	{
353	constraint ret = constraint_makeNew();
354	//constraintTerm term;
355
356	e = exprNode_fakeCopy(e);
357	ret->lexpr = constraintExpr_makeValueExpr (e);
358	ret->ar = EQ;
359	ret->post = TRUE;
360	ret->expr = constraintExpr_makeValueExpr (e);
361	ret->expr = constraintExpr_makeDecConstraintExpr (ret->expr);
362
363	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
364	// fileloc_incColumn ( ret->lexpr->term->loc);
365	// fileloc_incColumn ( ret->lexpr->term->loc);
366	return ret;
367	}
368	constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
369	{
370	constraint ret = constraint_makeNew();
371	//constraintTerm term;
372
373	e = exprNode_fakeCopy(e);
374	ret->lexpr = constraintExpr_makeValueExpr (e);
375	ret->ar = EQ;
376	ret->post = TRUE;
377	ret->expr = constraintExpr_makeValueExpr (e);
378	ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
379
380	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
381	// fileloc_incColumn ( ret->lexpr->term->loc);
382	// fileloc_incColumn ( ret->lexpr->term->loc);
383	return ret;
384	}
385
386
387
388	// constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
389	// {
390	// constraint ret = constraint_makeNew();
391	// //constraintTerm term;
392
393	// e = exprNode_fakeCopy(e);
394	// ret->lexpr = constraintExpr_makeMaxReadExpr(e);
395	// ret->ar = EQ;
396	// ret->post = TRUE;
397	// ret->expr = constraintExpr_makeIncConstraintExpr (e);
398	// ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
399	// return ret;
400	// }
401
402
403	cstring arithType_print (arithType ar)
404	{
405	cstring st = cstring_undefined;
406	switch (ar)
407	{
408	case LT:
409	st = cstring_makeLiteral (" < ");
410	break;
411	case LTE:
412	st = cstring_makeLiteral (" <= ");
413	break;
414	case GT:
415	st = cstring_makeLiteral (" > ");
416	break;
417	case GTE:
418	st = cstring_makeLiteral (" >= ");
419	break;
420	case EQ:
421	st = cstring_makeLiteral (" == ");
422	break;
423	case NONNEGATIVE:
424	st = cstring_makeLiteral (" NONNEGATIVE ");
425	break;
426	case POSITIVE:
427	st = cstring_makeLiteral (" POSITIVE ");
428	break;
429	default:
430	llassert(FALSE);
431	break;
432	}
433	return st;
434	}
435
436	void constraint_printError (constraint c, fileloc loc)
437	{
438	cstring string;
439
440	string = constraint_printDetailed (c);
441
442	if (c->post)
443	{
444	voptgenerror (FLG_FUNCTIONPOST, string, loc);
445	}
446	else
447	{
448	voptgenerror (FLG_FUNCTIONCONSTRAINT, string, loc);
449	}
450
451	}
452
453	cstring constraint_printDetailed (constraint c)
454	{
455	cstring st = cstring_undefined;
456
457
458	if (!c->post)
459	{
460	if (c->orig)
461	st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisfy %s", constraint_print (c), constraint_print(c->orig) );
462	else
463	st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
464
465	}
466	else
467	{
468	if (c->orig)
469	st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
470	else
471	st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));
472	}
473	return st;
474	}
475
476	cstring constraint_print (constraint c) /@/
477	{
478	cstring st = cstring_undefined;
479	cstring type = cstring_undefined;
480	llassert (c);
481	if (c->post)
482	{
483	type = cstring_makeLiteral ("Ensures: ");
484	}
485	else
486	{
487	type = cstring_makeLiteral ("Requires: ");
488	}
489	st = message ("%s: %s %s %s",
490	type,
491	constraintExpr_print (c->lexpr),
492	arithType_print(c->ar),
493	constraintExpr_print(c->expr)
494	);
495	return st;
496	}
497
498	constraint constraint_doSRefFixBaseParam (constraint precondition,
499	exprNodeList arglist)
500	{
501	precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
502	arglist);
503	precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
504	arglist);
505
506	return precondition;
507	}
508
509
510	constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
511	{
512	postcondition = constraint_copy (postcondition);
513	postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
514	postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
515
516	return postcondition;
517	}
518
519	constraint constraint_doSRefFixConstraintParam (constraint precondition,
520	exprNodeList arglist)
521	{
522
523	precondition = constraint_copy (precondition);
524	precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
525	precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
526
527	return precondition;
528	}
529
530	// bool constraint_hasTerm (constraint c, constraintTerm term)
531	// {
532	// DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
533
534	// if (constraintExpr_includesTerm (c->lexpr, term) )
535	// return TRUE;
536
537	// if (constraintExpr_includesTerm (c->expr, term) )
538	// return TRUE;
539
540	// return FALSE;
541	// }
542
543	constraint constraint_preserveOrig (constraint c)
544	{
545	c->orig = constraint_copy (c);
546	return c;
547	}
548	/@=fcnuse/
549	/@=assignexpose/
550	/@=czechfcns@/