constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint);
constraint constraint_makeSideEffectPostIncrement (exprNode t1, fileloc p_sequencePoint);
-
+void constraint_overWrite (constraint c1, constraint c2);
constraint constraint_copy (constraint c);
constraintExpr makePostOpInc (exprNode t1);
-
+bool fileloc_closer (fileloc loc1, fileloc loc2, fileloc loc3);
cstring constraintTerm_print (constraintTerm term);
cstring arithType_print (arithType ar);
cstring constraintExpr_print (constraintExpr ex);
fileloc constraint_getFileloc (constraint c);
cstring constraint_print (constraint c);
+constraint constraint_makeWriteSafeInt (exprNode po, int ind);
+
+exprNode exprNode_copyConstraints (exprNode dst, exprNode src);
+
+constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
+
+constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint);
+
/*@=czechfcns*/
#warning take this out
#include "constraintList.h"
#include "constraintExpr.h"
#include "constraintTerm.h"
-
+#include "constraintResolve.h"
#endif
extern constraintList constraintList_copy (constraintList s);
extern cstring constraintList_print (constraintList s);
+
+extern cstring
+constraintList_printDetailed (constraintList s);
+
+
+extern constraintList
+constraintList_logicalOr (constraintList l1, constraintList l2);
+
+extern constraintList constraintList_preserveOrig (constraintList c);
+
/*@constant int constraintListBASESIZE;@*/
+
+
# define constraintListBASESIZE SMALLBASESIZE
# else
environmentTable environment;
constraintList requiresConstraints;
constraintList ensuresConstraints;
+ //these two are used only for boolean expressions
+ //they store the ensures constraints for the true and false cases
+ constraintList trueEnsuresConstraints;
+ constraintList falseEnsuresConstraints;
} ;
/*@constant null exprNode exprNode_undefined; @*/
/*@only@*/ interfaceNodeList interfacelist;
/*@only@*/ CTypesNode ctypes;
} YYSTYPE;
-#define simpleOp 258
-#define PREFIX_OP 259
-#define POSTFIX_OP 260
-#define LLT_MULOP 261
-#define LLT_SEMI 262
-#define LLT_VERTICALBAR 263
-#define ITERATION_OP 264
-#define LLT_LPAR 265
-#define LLT_LBRACKET 266
-#define selectSym 267
-#define LLT_IF_THEN_ELSE 268
-#define logicalOp 269
-#define eqSepSym 270
-#define equationSym 271
-#define commentSym 272
-#define LLT_WHITESPACE 273
-#define LLT_EOL 274
-#define LLT_TYPEDEF_NAME 275
-#define quantifierSym 276
-#define openSym 277
-#define closeSym 278
-#define sepSym 279
-#define simpleId 280
-#define mapSym 281
-#define markerSym 282
-#define preSym 283
-#define postSym 284
-#define anySym 285
-#define LLT_COLON 286
-#define LLT_COMMA 287
-#define LLT_EQUALS 288
-#define LLT_LBRACE 289
-#define LLT_RBRACE 290
-#define LLT_RBRACKET 291
-#define LLT_RPAR 292
-#define LLT_QUOTE 293
-#define eqOp 294
-#define LLT_CCHAR 295
-#define LLT_CFLOAT 296
-#define LLT_CINTEGER 297
-#define LLT_LCSTRING 298
-#define LLT_ALL 299
-#define LLT_ANYTHING 300
-#define LLT_BE 301
-#define LLT_BODY 302
-#define LLT_CLAIMS 303
-#define LLT_CHECKS 304
-#define LLT_CONSTANT 305
-#define LLT_ELSE 306
-#define LLT_ENSURES 307
-#define LLT_FOR 308
-#define LLT_FRESH 309
-#define LLT_IF 310
-#define LLT_IMMUTABLE 311
-#define LLT_IMPORTS 312
-#define LLT_CONSTRAINT 313
-#define LLT_ISSUB 314
-#define LLT_LET 315
-#define LLT_MODIFIES 316
-#define LLT_MUTABLE 317
-#define LLT_NOTHING 318
-#define LLT_INTERNAL 319
-#define LLT_FILESYS 320
-#define LLT_OBJ 321
-#define LLT_OUT 322
-#define LLT_SEF 323
-#define LLT_ONLY 324
-#define LLT_PARTIAL 325
-#define LLT_OWNED 326
-#define LLT_DEPENDENT 327
-#define LLT_KEEP 328
-#define LLT_KEPT 329
-#define LLT_TEMP 330
-#define LLT_SHARED 331
-#define LLT_UNIQUE 332
-#define LLT_UNUSED 333
-#define LLT_EXITS 334
-#define LLT_MAYEXIT 335
-#define LLT_NEVEREXIT 336
-#define LLT_TRUEEXIT 337
-#define LLT_FALSEEXIT 338
-#define LLT_UNDEF 339
-#define LLT_KILLED 340
-#define LLT_CHECKMOD 341
-#define LLT_CHECKED 342
-#define LLT_UNCHECKED 343
-#define LLT_CHECKEDSTRICT 344
-#define LLT_TRUENULL 345
-#define LLT_FALSENULL 346
-#define LLT_LNULL 347
-#define LLT_LNOTNULL 348
-#define LLT_RETURNED 349
-#define LLT_OBSERVER 350
-#define LLT_EXPOSED 351
-#define LLT_REFCOUNTED 352
-#define LLT_REFS 353
-#define LLT_RELNULL 354
-#define LLT_RELDEF 355
-#define LLT_KILLREF 356
-#define LLT_NULLTERMINATED 357
-#define LLT_TEMPREF 358
-#define LLT_NEWREF 359
-#define LLT_PRIVATE 360
-#define LLT_REQUIRES 361
-#define LLT_RESULT 362
-#define LLT_SIZEOF 363
-#define LLT_SPEC 364
-#define LLT_TAGGEDUNION 365
-#define LLT_THEN 366
-#define LLT_TYPE 367
-#define LLT_TYPEDEF 368
-#define LLT_UNCHANGED 369
-#define LLT_USES 370
-#define LLT_CHAR 371
-#define LLT_CONST 372
-#define LLT_DOUBLE 373
-#define LLT_ENUM 374
-#define LLT_FLOAT 375
-#define LLT_INT 376
-#define LLT_ITER 377
-#define LLT_YIELD 378
-#define LLT_LONG 379
-#define LLT_SHORT 380
-#define LLT_SIGNED 381
-#define LLT_UNKNOWN 382
-#define LLT_STRUCT 383
-#define LLT_TELIPSIS 384
-#define LLT_UNION 385
-#define LLT_UNSIGNED 386
-#define LLT_VOID 387
-#define LLT_VOLATILE 388
-#define LLT_PRINTFLIKE 389
-#define LLT_SCANFLIKE 390
-#define LLT_MESSAGELIKE 391
+#define simpleOp 257
+#define PREFIX_OP 258
+#define POSTFIX_OP 259
+#define LLT_MULOP 260
+#define LLT_SEMI 261
+#define LLT_VERTICALBAR 262
+#define ITERATION_OP 263
+#define LLT_LPAR 264
+#define LLT_LBRACKET 265
+#define selectSym 266
+#define LLT_IF_THEN_ELSE 267
+#define logicalOp 268
+#define eqSepSym 269
+#define equationSym 270
+#define commentSym 271
+#define LLT_WHITESPACE 272
+#define LLT_EOL 273
+#define LLT_TYPEDEF_NAME 274
+#define quantifierSym 275
+#define openSym 276
+#define closeSym 277
+#define sepSym 278
+#define simpleId 279
+#define mapSym 280
+#define markerSym 281
+#define preSym 282
+#define postSym 283
+#define anySym 284
+#define LLT_COLON 285
+#define LLT_COMMA 286
+#define LLT_EQUALS 287
+#define LLT_LBRACE 288
+#define LLT_RBRACE 289
+#define LLT_RBRACKET 290
+#define LLT_RPAR 291
+#define LLT_QUOTE 292
+#define eqOp 293
+#define LLT_CCHAR 294
+#define LLT_CFLOAT 295
+#define LLT_CINTEGER 296
+#define LLT_LCSTRING 297
+#define LLT_ALL 298
+#define LLT_ANYTHING 299
+#define LLT_BE 300
+#define LLT_BODY 301
+#define LLT_CLAIMS 302
+#define LLT_CHECKS 303
+#define LLT_CONSTANT 304
+#define LLT_ELSE 305
+#define LLT_ENSURES 306
+#define LLT_FOR 307
+#define LLT_FRESH 308
+#define LLT_IF 309
+#define LLT_IMMUTABLE 310
+#define LLT_IMPORTS 311
+#define LLT_CONSTRAINT 312
+#define LLT_ISSUB 313
+#define LLT_LET 314
+#define LLT_MODIFIES 315
+#define LLT_MUTABLE 316
+#define LLT_NOTHING 317
+#define LLT_INTERNAL 318
+#define LLT_FILESYS 319
+#define LLT_OBJ 320
+#define LLT_OUT 321
+#define LLT_SEF 322
+#define LLT_ONLY 323
+#define LLT_PARTIAL 324
+#define LLT_OWNED 325
+#define LLT_DEPENDENT 326
+#define LLT_KEEP 327
+#define LLT_KEPT 328
+#define LLT_TEMP 329
+#define LLT_SHARED 330
+#define LLT_UNIQUE 331
+#define LLT_UNUSED 332
+#define LLT_EXITS 333
+#define LLT_MAYEXIT 334
+#define LLT_NEVEREXIT 335
+#define LLT_TRUEEXIT 336
+#define LLT_FALSEEXIT 337
+#define LLT_UNDEF 338
+#define LLT_KILLED 339
+#define LLT_CHECKMOD 340
+#define LLT_CHECKED 341
+#define LLT_UNCHECKED 342
+#define LLT_CHECKEDSTRICT 343
+#define LLT_TRUENULL 344
+#define LLT_FALSENULL 345
+#define LLT_LNULL 346
+#define LLT_LNOTNULL 347
+#define LLT_RETURNED 348
+#define LLT_OBSERVER 349
+#define LLT_EXPOSED 350
+#define LLT_REFCOUNTED 351
+#define LLT_REFS 352
+#define LLT_RELNULL 353
+#define LLT_RELDEF 354
+#define LLT_KILLREF 355
+#define LLT_NULLTERMINATED 356
+#define LLT_TEMPREF 357
+#define LLT_NEWREF 358
+#define LLT_PRIVATE 359
+#define LLT_REQUIRES 360
+#define LLT_RESULT 361
+#define LLT_SIZEOF 362
+#define LLT_SPEC 363
+#define LLT_TAGGEDUNION 364
+#define LLT_THEN 365
+#define LLT_TYPE 366
+#define LLT_TYPEDEF 367
+#define LLT_UNCHANGED 368
+#define LLT_USES 369
+#define LLT_CHAR 370
+#define LLT_CONST 371
+#define LLT_DOUBLE 372
+#define LLT_ENUM 373
+#define LLT_FLOAT 374
+#define LLT_INT 375
+#define LLT_ITER 376
+#define LLT_YIELD 377
+#define LLT_LONG 378
+#define LLT_SHORT 379
+#define LLT_SIGNED 380
+#define LLT_UNKNOWN 381
+#define LLT_STRUCT 382
+#define LLT_TELIPSIS 383
+#define LLT_UNION 384
+#define LLT_UNSIGNED 385
+#define LLT_VOID 386
+#define LLT_VOLATILE 387
+#define LLT_PRINTFLIKE 388
+#define LLT_SCANFLIKE 389
+#define LLT_MESSAGELIKE 390
extern YYSTYPE yllval;
/*@only@*/ interfaceNodeList interfacelist;
/*@only@*/ CTypesNode ctypes;
} YYSTYPE;
-#define simpleOp 258
-#define PREFIX_OP 259
-#define POSTFIX_OP 260
-#define LLT_MULOP 261
-#define LLT_SEMI 262
-#define LLT_VERTICALBAR 263
-#define ITERATION_OP 264
-#define LLT_LPAR 265
-#define LLT_LBRACKET 266
-#define selectSym 267
-#define LLT_IF_THEN_ELSE 268
-#define logicalOp 269
-#define eqSepSym 270
-#define equationSym 271
-#define commentSym 272
-#define LLT_WHITESPACE 273
-#define LLT_EOL 274
-#define LLT_TYPEDEF_NAME 275
-#define quantifierSym 276
-#define openSym 277
-#define closeSym 278
-#define sepSym 279
-#define simpleId 280
-#define mapSym 281
-#define markerSym 282
-#define preSym 283
-#define postSym 284
-#define anySym 285
-#define LLT_COLON 286
-#define LLT_COMMA 287
-#define LLT_EQUALS 288
-#define LLT_LBRACE 289
-#define LLT_RBRACE 290
-#define LLT_RBRACKET 291
-#define LLT_RPAR 292
-#define LLT_QUOTE 293
-#define eqOp 294
-#define LLT_CCHAR 295
-#define LLT_CFLOAT 296
-#define LLT_CINTEGER 297
-#define LLT_LCSTRING 298
-#define LLT_ALL 299
-#define LLT_ANYTHING 300
-#define LLT_BE 301
-#define LLT_BODY 302
-#define LLT_CLAIMS 303
-#define LLT_CHECKS 304
-#define LLT_CONSTANT 305
-#define LLT_ELSE 306
-#define LLT_ENSURES 307
-#define LLT_FOR 308
-#define LLT_FRESH 309
-#define LLT_IF 310
-#define LLT_IMMUTABLE 311
-#define LLT_IMPORTS 312
-#define LLT_CONSTRAINT 313
-#define LLT_ISSUB 314
-#define LLT_LET 315
-#define LLT_MODIFIES 316
-#define LLT_MUTABLE 317
-#define LLT_NOTHING 318
-#define LLT_INTERNAL 319
-#define LLT_FILESYS 320
-#define LLT_OBJ 321
-#define LLT_OUT 322
-#define LLT_SEF 323
-#define LLT_ONLY 324
-#define LLT_PARTIAL 325
-#define LLT_OWNED 326
-#define LLT_DEPENDENT 327
-#define LLT_KEEP 328
-#define LLT_KEPT 329
-#define LLT_TEMP 330
-#define LLT_SHARED 331
-#define LLT_UNIQUE 332
-#define LLT_UNUSED 333
-#define LLT_EXITS 334
-#define LLT_MAYEXIT 335
-#define LLT_NEVEREXIT 336
-#define LLT_TRUEEXIT 337
-#define LLT_FALSEEXIT 338
-#define LLT_UNDEF 339
-#define LLT_KILLED 340
-#define LLT_CHECKMOD 341
-#define LLT_CHECKED 342
-#define LLT_UNCHECKED 343
-#define LLT_CHECKEDSTRICT 344
-#define LLT_TRUENULL 345
-#define LLT_FALSENULL 346
-#define LLT_LNULL 347
-#define LLT_LNOTNULL 348
-#define LLT_RETURNED 349
-#define LLT_OBSERVER 350
-#define LLT_EXPOSED 351
-#define LLT_REFCOUNTED 352
-#define LLT_REFS 353
-#define LLT_RELNULL 354
-#define LLT_RELDEF 355
-#define LLT_KILLREF 356
-#define LLT_NULLTERMINATED 357
-#define LLT_TEMPREF 358
-#define LLT_NEWREF 359
-#define LLT_PRIVATE 360
-#define LLT_REQUIRES 361
-#define LLT_RESULT 362
-#define LLT_SIZEOF 363
-#define LLT_SPEC 364
-#define LLT_TAGGEDUNION 365
-#define LLT_THEN 366
-#define LLT_TYPE 367
-#define LLT_TYPEDEF 368
-#define LLT_UNCHANGED 369
-#define LLT_USES 370
-#define LLT_CHAR 371
-#define LLT_CONST 372
-#define LLT_DOUBLE 373
-#define LLT_ENUM 374
-#define LLT_FLOAT 375
-#define LLT_INT 376
-#define LLT_ITER 377
-#define LLT_YIELD 378
-#define LLT_LONG 379
-#define LLT_SHORT 380
-#define LLT_SIGNED 381
-#define LLT_UNKNOWN 382
-#define LLT_STRUCT 383
-#define LLT_TELIPSIS 384
-#define LLT_UNION 385
-#define LLT_UNSIGNED 386
-#define LLT_VOID 387
-#define LLT_VOLATILE 388
-#define LLT_PRINTFLIKE 389
-#define LLT_SCANFLIKE 390
-#define LLT_MESSAGELIKE 391
+#define simpleOp 257
+#define PREFIX_OP 258
+#define POSTFIX_OP 259
+#define LLT_MULOP 260
+#define LLT_SEMI 261
+#define LLT_VERTICALBAR 262
+#define ITERATION_OP 263
+#define LLT_LPAR 264
+#define LLT_LBRACKET 265
+#define selectSym 266
+#define LLT_IF_THEN_ELSE 267
+#define logicalOp 268
+#define eqSepSym 269
+#define equationSym 270
+#define commentSym 271
+#define LLT_WHITESPACE 272
+#define LLT_EOL 273
+#define LLT_TYPEDEF_NAME 274
+#define quantifierSym 275
+#define openSym 276
+#define closeSym 277
+#define sepSym 278
+#define simpleId 279
+#define mapSym 280
+#define markerSym 281
+#define preSym 282
+#define postSym 283
+#define anySym 284
+#define LLT_COLON 285
+#define LLT_COMMA 286
+#define LLT_EQUALS 287
+#define LLT_LBRACE 288
+#define LLT_RBRACE 289
+#define LLT_RBRACKET 290
+#define LLT_RPAR 291
+#define LLT_QUOTE 292
+#define eqOp 293
+#define LLT_CCHAR 294
+#define LLT_CFLOAT 295
+#define LLT_CINTEGER 296
+#define LLT_LCSTRING 297
+#define LLT_ALL 298
+#define LLT_ANYTHING 299
+#define LLT_BE 300
+#define LLT_BODY 301
+#define LLT_CLAIMS 302
+#define LLT_CHECKS 303
+#define LLT_CONSTANT 304
+#define LLT_ELSE 305
+#define LLT_ENSURES 306
+#define LLT_FOR 307
+#define LLT_FRESH 308
+#define LLT_IF 309
+#define LLT_IMMUTABLE 310
+#define LLT_IMPORTS 311
+#define LLT_CONSTRAINT 312
+#define LLT_ISSUB 313
+#define LLT_LET 314
+#define LLT_MODIFIES 315
+#define LLT_MUTABLE 316
+#define LLT_NOTHING 317
+#define LLT_INTERNAL 318
+#define LLT_FILESYS 319
+#define LLT_OBJ 320
+#define LLT_OUT 321
+#define LLT_SEF 322
+#define LLT_ONLY 323
+#define LLT_PARTIAL 324
+#define LLT_OWNED 325
+#define LLT_DEPENDENT 326
+#define LLT_KEEP 327
+#define LLT_KEPT 328
+#define LLT_TEMP 329
+#define LLT_SHARED 330
+#define LLT_UNIQUE 331
+#define LLT_UNUSED 332
+#define LLT_EXITS 333
+#define LLT_MAYEXIT 334
+#define LLT_NEVEREXIT 335
+#define LLT_TRUEEXIT 336
+#define LLT_FALSEEXIT 337
+#define LLT_UNDEF 338
+#define LLT_KILLED 339
+#define LLT_CHECKMOD 340
+#define LLT_CHECKED 341
+#define LLT_UNCHECKED 342
+#define LLT_CHECKEDSTRICT 343
+#define LLT_TRUENULL 344
+#define LLT_FALSENULL 345
+#define LLT_LNULL 346
+#define LLT_LNOTNULL 347
+#define LLT_RETURNED 348
+#define LLT_OBSERVER 349
+#define LLT_EXPOSED 350
+#define LLT_REFCOUNTED 351
+#define LLT_REFS 352
+#define LLT_RELNULL 353
+#define LLT_RELDEF 354
+#define LLT_KILLREF 355
+#define LLT_NULLTERMINATED 356
+#define LLT_TEMPREF 357
+#define LLT_NEWREF 358
+#define LLT_PRIVATE 359
+#define LLT_REQUIRES 360
+#define LLT_RESULT 361
+#define LLT_SIZEOF 362
+#define LLT_SPEC 363
+#define LLT_TAGGEDUNION 364
+#define LLT_THEN 365
+#define LLT_TYPE 366
+#define LLT_TYPEDEF 367
+#define LLT_UNCHANGED 368
+#define LLT_USES 369
+#define LLT_CHAR 370
+#define LLT_CONST 371
+#define LLT_DOUBLE 372
+#define LLT_ENUM 373
+#define LLT_FLOAT 374
+#define LLT_INT 375
+#define LLT_ITER 376
+#define LLT_YIELD 377
+#define LLT_LONG 378
+#define LLT_SHORT 379
+#define LLT_SIGNED 380
+#define LLT_UNKNOWN 381
+#define LLT_STRUCT 382
+#define LLT_TELIPSIS 383
+#define LLT_UNION 384
+#define LLT_UNSIGNED 385
+#define LLT_VOID 386
+#define LLT_VOLATILE 387
+#define LLT_PRINTFLIKE 388
+#define LLT_SCANFLIKE 389
+#define LLT_MESSAGELIKE 390
extern YYSTYPE yllval;
extern bool lltok_isSemi (lltok p_tok);
+/* DRL added 10/23/2000 for boolean stuff */
+extern bool lltok_isEq_Op (lltok tok);
+
# else
# error "Multiple include"
# endif
+
@echo '// '
$(CC) -o lclint $(OBJ) $(LINKFLAGS)
+object: $(OBJ)
+
+mylint:
+ CC="$(LCLINT)" ; export CC ; $(MAKE) -e object
###
### grammars
###
@echo '// '
@$(MAKE) -e opt
@echo '// Done Release '`cat $(VERSION_NUMBER)`
-
+
###
### cleaning
###
-###
-### If I was smarter, I'd figure out how to get configure to fill in the
-### variables here instead of using environment variables to override
-### them. The way I do it is pretty lame....
-###
-
################################################
###
### Generic system dependant Makefile
OFILES = $(LS) *.o | $(WC) -l
SFILES = $(LS) *.c | $(WC) -l
+## on mamba
+#BISON = /usr/local/bin/bison
+#FLEX = /usr/local/bin/flex
+
+BISON = /usr/bin/bison
+FLEX = /usr/bin/flex
+
+# ${HOME}/bison-1.28/bin/bison
+
+
###
### Compiler and compiler flags
###
### NOTE: CC is set in top level Makefile
###
-CC = gcc
-CCOPT = gcc -O2
+CC = /usr/local/bin/gcc -Wall -g
+CCOPT = /usr/local/bin/gcc -Wall -g
+# -O4 doesn't work with bison 1.25
###
### CPPFLAGS also used by lclint --- it should only include -I, -D and
CPPFLAGS = -I$(HEADERDIR) -DUNIX -DNOSTDLIB=0 -DUGS=1
### -DUGS=1 is needed for AIX (should be set by configure)
-### lex library (overrode by configure environment variable)
-LINKFLAGS = -ll
+### lex library
+
+LINKFLAGS = -lfl
+
ifeq ($(CC), gcc)
CFLAGS = $(CPPFLAGS) -Wpointer-arith -Wcast-qual -Wcomment -Wswitch -Wunused -Wreturn-type -ansi -pedantic
DEBUGFLAGS = -DYYDEBUG=1 -DYYIMPURE=1 # don't change this
-BISON = /af10/evans/bison-1.28/bin/bison
-FLEX = /usr/bin/flex
-
### bison flags
-YFLAGS = -v -t -d
+YFLAGS = -v -t -d --debug
###
### controls lclint checking (uncomment this line to have
VERSION_NUMBER = lastversion
+###
+### Defaults (overrode by environment varialbles for local build)
+###
-
+SYSTEM_LIBDIR = /usr/include
+DEFAULT_LARCHPATH = /usr/local/lclint-2.5m/lib
+DEFAULT_LCLIMPORTDIR = /usr/local/lclint-2.5m/imports
}
+/* make constraint ensures e1 == e2 */
+
+constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
+{
+ constraint ret = constraint_makeNew();
+ exprNode e;
+
+ e = exprNode_fakeCopy(e1);
+ ret->lexpr = constraintExpr_makeValueExpr (e);
+ ret->ar = EQ;
+ ret->post = TRUE;
+ e = exprNode_fakeCopy(e2);
+ ret->expr = constraintExpr_makeValueExpr (e);
+
+ ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+// fileloc_incColumn ( ret->lexpr->term->loc);
+// fileloc_incColumn ( ret->lexpr->term->loc);
+ return ret;
+}
+
+
+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();
ret->expr = constraintExpr_makeValueExpr (e);
ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
- ret->expr = constraintExpr_setFileloc (ret->expr, sequencePoint);
+ 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();
}
else
{
- st = message ("Function Post condition:\nThis function appears to have the post condition %s\n based on %s", constraint_print (c), constraint_print(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) );
}
return st;
}
//static void exprNode_constraintPropagateUp (exprNode p_e);
constraintList exprNode_traversRequiresConstraints (exprNode e);
constraintList exprNode_traversEnsuresConstraints (exprNode e);
+
+constraintList exprNode_traversTrueEnsuresConstraints (exprNode e);
+
+extern constraintList reflectChanges (constraintList pre2, constraintList post1);
+
void mergeResolve (exprNode parent, exprNode child1, exprNode child2);
case XPR_CASE:
case XPR_INIT:
case XPR_NODE:
- DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) );
- return FALSE;
+ TPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) );
+ return TRUE;
/*@notreached@*/
break;
default:
- return TRUE;
+ return FALSE;
}
/*not reached*/
bool exprNode_handleError( exprNode e)
{
- if (exprNode_isError (e) || !exprNode_isUnhandled(e) )
+ if (exprNode_isError (e) || exprNode_isUnhandled(e) )
{
static /*@only@*/ cstring error = cstring_undefined;
void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e)
{
- DPRINTF((message ("exprNode_gnerateConstraints Analysising %s %s at", exprNode_unparse( e),
- fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
+ if (exprNode_isError (e) )
+ return FALSE;
+ if (exprNode_isUnhandled (e) )
+ {
+ TPRINTF( (message("Warning ignoring %s", exprNode_unparse (e) ) ) );
+ e->requiresConstraints = constraintList_new();
+ e->ensuresConstraints = constraintList_new();
+ e->trueEnsuresConstraints = constraintList_new();
+ e->falseEnsuresConstraints = constraintList_new();
+ llassert(FALSE);
+ return FALSE;
+ }
+
+
+
+ TPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e),
+ fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
+
if (exprNode_isMultiStatement ( e) )
{
exprNode_multiStatement(e);
}
else
{
- llassert(FALSE);
+ // llassert(FALSE);
+ return FALSE;
}
printf ("%s", (message ("%s", constraintList_printDetailed (e->requiresConstraints) ) ) );
printf ("%s", (message ("%s", constraintList_printDetailed (e->ensuresConstraints) ) ) );
if (e->kind != XPR_STMT)
{
- DPRINTF (("Not Stmt") );
- DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
+ TPRINTF (("Not Stmt") );
+ TPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
if (exprNode_isMultiStatement (e) )
{
return exprNode_multiStatement (e );
}
- llassert(FALSE);
+ // llassert(FALSE);
}
- DPRINTF (("Stmt") );
- DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
+ TPRINTF (("Stmt") );
+ TPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
snode = exprData_getUopNode (e->edata);
if (exprNode_isMultiStatement (snode))
{
- llassert(FALSE);
+ // llassert(FALSE);
return exprNode_multiStatement (snode);
}
printf ("%s\n", constraintList_print(e->requiresConstraints) );
e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode);
printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
- llassert(notError);
+ // llassert(notError);
return notError;
}
return exprNode_stmt(e);
}
llassert (e->kind == XPR_STMTLIST);
- DPRINTF(( "STMTLIST:") );
- DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
+ TPRINTF(( "STMTLIST:") );
+ TPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
stmt1 = exprData_getPairA (e->edata);
stmt2 = exprData_getPairB (e->edata);
- DPRINTF(("XW stmtlist ") );
+ DPRINTF((" stmtlist ") );
DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) );
exprNode_stmt (stmt1);
}
+exprNode doIf (exprNode e, exprNode test, exprNode body)
+{
+ test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
+ e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints);
+ e->requiresConstraints = reflectChanges (e->requiresConstraints,
+ test->ensuresConstraints);
+#warning bad
+ e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
+ return e;
+}
+
bool exprNode_multiStatement (exprNode e)
{
bool ret;
exprData data;
-
+ exprNode e1, e2;
+ exprNode p, trueBranch, falseBranch;
+ exprNode forPred, forBody;
+ exprNode init, test, inc;
+ constraintList cons;
+ constraintList t, f;
+ e->requiresConstraints = constraintList_new();
+ e->ensuresConstraints = constraintList_new();
+ e->trueEnsuresConstraints = constraintList_new();
+ e->falseEnsuresConstraints = constraintList_new();
+
DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
{
case XPR_FOR:
- // ret = message ("%s %s",
- exprNode_generateConstraints (exprData_getPairA (data));
- exprNode_generateConstraints (exprData_getPairB (data));
+ // ret = message ("%s %s",
+ forPred = exprData_getPairA (data);
+ forBody = exprData_getPairB (data);
+
+
+ //first generate the constraints
+ exprNode_generateConstraints (forPred);
+ exprNode_generateConstraints (forBody);
+
+ //merge the constraints: modle as if statement
+ /* init
+ if (test)
+ for body
+ inc */
+ init = exprData_getTripleInit (forPred->edata);
+ test = exprData_getTripleTest (forPred->edata);
+ inc = exprData_getTripleInc (forPred->edata);
+
+ test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
+ // e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints);
+ e->requiresConstraints = reflectChanges (e->requiresConstraints, test->ensuresConstraints);
+
break;
case XPR_FORPRED:
// ret = message ("for (%s; %s; %s)",
- exprNode_generateConstraints (exprData_getTripleInit (data));
- exprNode_generateConstraints (exprData_getTripleTest (data));
- exprNode_generateConstraints (exprData_getTripleInc (data));
+ exprNode_generateConstraints (exprData_getTripleInit (data) );
+ exprNode_exprTraverse (exprData_getTripleTest (data),FALSE, FALSE, exprNode_loc(e));
+ exprNode_generateConstraints (exprData_getTripleInc (data));
break;
case XPR_IF:
- DPRINTF(( "IF:") );
- DPRINTF ((exprNode_unparse(e) ) );
- // ret = message ("if (%s) %s",
- exprNode_generateConstraints (exprData_getPairA (data));
- exprNode_generateConstraints (exprData_getPairB (data));
- // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
+ TPRINTF(( "IF:") );
+ TPRINTF ((exprNode_unparse(e) ) );
+ // ret = message ("if (%s) %s",
+ e1 = exprData_getPairA (data);
+ e2 = exprData_getPairB (data);
+
+ exprNode_exprTraverse (e1,
+ FALSE, FALSE, exprNode_loc(e1));
+
+ exprNode_generateConstraints (e2);
+
+ e = doIf (e, e1, e2);
+
+
+ // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
break;
case XPR_IFELSE:
+ TPRINTF(("Starting IFELSE"));
// ret = message ("if (%s) %s else %s",
- exprNode_generateConstraints (exprData_getTriplePred (data));
- exprNode_generateConstraints (exprData_getTripleTrue (data));
- exprNode_generateConstraints (exprData_getTripleFalse (data));
+ p = exprData_getTriplePred (data);
+ trueBranch = exprData_getTripleTrue (data);
+ falseBranch = exprData_getTripleFalse (data);
+
+ exprNode_exprTraverse (p,
+ FALSE, FALSE, exprNode_loc(p));
+ exprNode_generateConstraints (trueBranch);
+ exprNode_generateConstraints (falseBranch);
+
+ // do requires clauses
+
+ cons = reflectChanges (trueBranch->requiresConstraints, p->trueEnsuresConstraints);
+ cons = reflectChanges (cons,
+ p->ensuresConstraints);
+ e->requiresConstraints = constraintList_copy (cons);
+
+ cons = reflectChanges (falseBranch->requiresConstraints, p->falseEnsuresConstraints);
+ cons = reflectChanges (cons,
+ p->ensuresConstraints);
+ e->requiresConstraints = constraintList_addList (e->requiresConstraints,
+ cons);
+ e->requiresConstraints = constraintList_addList (e->requiresConstraints,
+ p->requiresConstraints);
+
+ // do ensures clauses
+ // find the the ensures lists for each subbranch
+ t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints);
+ t = constraintList_mergeEnsures (p->ensuresConstraints, t);
+
+ f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints);
+ f = constraintList_mergeEnsures (p->ensuresConstraints, f);
+
+ // find ensures for whole if/else statement
+
+ e->ensuresConstraints = constraintList_logicalOr (t, f);
+ TPRINTF( ("Done IFELSE") );
break;
case XPR_WHILE:
+ e1 = exprData_getPairA (data);
+ e2 = exprData_getPairB (data);
+ exprNode_exprTraverse (e1,
+ FALSE, FALSE, exprNode_loc(e1));
+
+ exprNode_generateConstraints (e2);
+
+ e1->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(e1);
+
+ e->requiresConstraints = reflectChanges (e2->requiresConstraints, e1->trueEnsuresConstraints);
+
+ e->requiresConstraints = reflectChanges (e->requiresConstraints,
+ e1->ensuresConstraints);
+#warning bad
+ e->ensuresConstraints = constraintList_copy (e1->ensuresConstraints);
+
// ret = message ("while (%s) %s",
exprNode_generateConstraints (exprData_getPairA (data));
exprNode_generateConstraints (exprData_getPairB (data));
// e->constraints = constraintList_exprNodemerge (exprData_getPairA (data), exprData_getPairB (data) );
break;
- case XPR_WHILEPRED:
- // ret =
- // cstring_copy (
- exprNode_generateConstraints (exprData_getSingle (data));
- break;
-
case XPR_DOWHILE:
// ret = message ("do { %s } while (%s)",
exprNode_generateConstraints (exprData_getPairB (data));
bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint)
{
exprNode t1, t2;
-
+ lltok tok;
bool handledExprNode;
exprData data;
constraint cons;
-
- DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
- fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
+ constraintList tempList;
- e->requiresConstraints = constraintList_new();
- e->ensuresConstraints = constraintList_new();
-
- if (exprNode_handleError (e))
+ if (exprNode_handleError (e))
{
return FALSE;
}
+
+ TPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
+ fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
+
+ e->requiresConstraints = constraintList_new();
+ e->ensuresConstraints = constraintList_new();
+ e->trueEnsuresConstraints = constraintList_new();;
+ e->falseEnsuresConstraints = constraintList_new();;
+
handledExprNode = TRUE;
switch (e->kind)
{
+
+ case XPR_WHILEPRED:
+ t1 = exprData_getSingle (data);
+ exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
+ e = exprNode_copyConstraints (e, t1);
+ break;
+
case XPR_FETCH:
if (definatelv )
break;
case XPR_PREOP:
t1 = exprData_getUopNode(data);
- lltok_unparse (exprData_getUopTok (data));
- exprNode_exprTraverse (exprData_getUopNode (data), definatelv, definaterv, sequencePoint );
+ //lltok_unparse (exprData_getUopTok (data));
+ exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
/*handle * pointer access */
/*@ i 325 do ++ and -- */
}
e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
}
- if (lltok_isInc_Op (exprData_getUopTok (data) ) )
+
+ /* ! expr */
+ if (lltok_isNot_Op (exprData_getUopTok (data) ) )
{
- // cons = constraint_makeSideEffectPostIncrement (t1, sequencePoint);
- // e->ensuresConstraints = constraintList_add(e->requiresConstraints, cons);
+ e->trueEnsuresConstraints = constraintList_copy (t1->falseEnsuresConstraints);
+ e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
}
break;
// e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
break;
case XPR_ASSIGN:
- exprNode_exprTraverse (exprData_getOpA (data), TRUE, definaterv, sequencePoint );
+ t1 = exprData_getOpA (data);
+ t2 = exprData_getOpB (data);
+ exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
lltok_unparse (exprData_getOpTok (data));
- exprNode_exprTraverse (exprData_getOpB (data), definatelv, TRUE, sequencePoint );
- // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data) );
+ exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
+
+ // TPRINTF ( ("Doing ASSign"));
+ cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
+
+ e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
+
break;
case XPR_OP:
- exprNode_exprTraverse (exprData_getOpA (data), definatelv, definaterv, sequencePoint );
- lltok_unparse (exprData_getOpTok (data));
- exprNode_exprTraverse (exprData_getOpB (data), definatelv, definaterv, sequencePoint );
+ t1 = exprData_getOpA (data);
+ t2 = exprData_getOpB (data);
+ exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
+ tok = exprData_getOpTok (data);
+ exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
+ if (lltok_isEq_Op (tok) )
+ {
+ cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
+ e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
+ }
+ if (lltok_isAnd_Op (tok) )
+ {
+ //true ensures
+ tempList = constraintList_copy (t1->trueEnsuresConstraints);
+ tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
+ e->trueEnsuresConstraints = constraintList_addList(e->trueEnsuresConstraints, tempList);
+
+ //false ensures: fens t1 or tens t1 and fens t2
+ tempList = constraintList_copy (t1->trueEnsuresConstraints);
+ tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
+ tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
+ e->falseEnsuresConstraints =constraintList_addList(e->falseEnsuresConstraints, tempList);
+
+ }
+ if (lltok_isOr_Op (tok) )
+ {
+ //false ensures
+ tempList = constraintList_copy (t1->falseEnsuresConstraints);
+ tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
+ e->falseEnsuresConstraints = constraintList_addList(e->falseEnsuresConstraints, tempList);
+
+ //true ensures: tens t1 or fens t1 and tens t2
+ tempList = constraintList_copy (t1->falseEnsuresConstraints);
+ tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
+ tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
+ e->trueEnsuresConstraints =constraintList_addList(e->trueEnsuresConstraints, tempList);
+
+ }
+
// e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
break;
case XPR_SIZEOFT:
return handledExprNode;
}
+
+constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
+{
+ // exprNode t1, t2;
+
+ bool handledExprNode;
+ // char * mes;
+ exprData data;
+ constraintList ret;
+ ret = constraintList_copy (e->trueEnsuresConstraints );
+ if (exprNode_handleError (e))
+ {
+ return ret;
+ }
+
+ handledExprNode = TRUE;
+
+ data = e->edata;
+
+ switch (e->kind)
+ {
+
+ case XPR_FETCH:
+
+ ret = constraintList_addList (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getPairA (data) ) );
+
+ ret = constraintList_addList (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getPairB (data) ) );
+ break;
+ case XPR_PREOP:
+
+ ret = constraintList_addList (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getUopNode (data) ) );
+ break;
+
+ case XPR_PARENS:
+ ret = constraintList_addList (ret, exprNode_traversTrueEnsuresConstraints
+ (exprData_getUopNode (data) ) );
+ break;
+ case XPR_ASSIGN:
+ ret = constraintList_addList (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getOpA (data) ) );
+
+ ret = constraintList_addList (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getOpB (data) ) );
+ break;
+ case XPR_OP:
+ ret = constraintList_addList (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getOpA (data) ) );
+
+ ret = constraintList_addList (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getOpB (data) ) );
+ break;
+ case XPR_SIZEOFT:
+
+ // ctype_unparse (qtype_getType (exprData_getType (data) ) );
+
+ break;
+
+ case XPR_SIZEOF:
+
+ ret = constraintList_addList (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getSingle (data) ) );
+ break;
+
+ case XPR_CALL:
+ ret = constraintList_addList (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getFcn (data) ) );
+ /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
+ break;
+
+ case XPR_RETURN:
+ ret = constraintList_addList (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getSingle (data) ) );
+ break;
+
+ case XPR_NULLRETURN:
+ // cstring_makeLiteral ("return");;
+ break;
+
+ case XPR_FACCESS:
+ ret = constraintList_addList (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getFieldNode (data) ) );
+ //exprData_getFieldName (data) ;
+ break;
+
+ case XPR_ARROW:
+ ret = constraintList_addList (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getFieldNode (data) ) );
+ // exprData_getFieldName (data);
+ break;
+
+ case XPR_STRINGLITERAL:
+ // cstring_copy (exprData_getLiteral (data));
+ break;
+
+ case XPR_NUMLIT:
+ // cstring_copy (exprData_getLiteral (data));
+ break;
+ case XPR_POSTOP:
+
+ ret = constraintList_addList (ret,
+ exprNode_traversTrueEnsuresConstraints
+ (exprData_getUopNode (data) ) );
+ break;
+ default:
+ break;
+ }
+
+ return ret;
+}
+
+
/* walk down the tree and get all requires Constraints in each subexpression*/
constraintList exprNode_traversRequiresConstraints (exprNode e)
{
void constraintList_debugPrint ( char * s )
{
- TPRINTF((s) );
+ DPRINTF((s) );
}
void constraint_print (constraint c)
e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
if (lltok_isInc_Op (exprData_getUopTok (data) ) )
{
- TPRINTF(("++ -- will be implemented later"));
+ DPRINTF(("++ -- will be implemented later"));
// e->constraints = constraintList_add( e->constraints,
// constraint_makeInc_Op (exprData_getUopNode (data) ) );
}
break;
default:
- TPRINTF(("no special constraint generation"));
+ DPRINTF(("no special constraint generation"));
ret = NULL;
}
constraintList
constraintList_add (constraintList s, constraint el)
{
+ if (resolve (el, s) )
+ return s;
+
if (s->nspace <= 0)
constraintList_grow (s);
return st;
}
+/*{ x: constraint | (x in l1 -> resolve (x, l2) || (x in l2 -> resolve (x, l1)
+} */
+
+constraintList
+constraintList_logicalOr (constraintList l1, constraintList l2)
+{
+ constraint temp;
+ constraintList ret;
+ TPRINTF ( (message ("Logical of on %s and %s",
+ constraintList_print(l1),
+ constraintList_print(l2)) ) );
+
+ ret = constraintList_new();
+ constraintList_elements (l1, el)
+ {
+ temp = substitute (el, l2);
+
+ if (resolve (el, l2) || resolve(temp,l2) )
+ { /*avoid redundant constraints*/
+ if (!resolve (el, ret) )
+ ret = constraintList_add (ret, el);
+ }
+ }
+ end_constraintList_elements;
+
+ constraintList_elements (l2, el)
+ {
+ temp = substitute (el, l1);
+
+ if (resolve (el, l1) || resolve(temp,l1) )
+ {
+ /*avoid redundant constraints*/
+ if (!resolve (el, ret) )
+ ret = constraintList_add (ret, el);
+ }
+ }
+ end_constraintList_elements;
+
+
+ return ret;
+}
+
void
constraintList_free (constraintList s)
{
/*
-/*
+*
** constraintResolve.c
*/
constraintList reflectChangesEnsures (constraintList pre2, constraintList post1);
constraint constraint_simplify (constraint c);
+constraintList constraintList_fixConflicts (constraintList list1, constraintList list2);
+
+constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2);
+
+constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2);
+
+
+/*********************************************/
+
+
+constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2)
+{
+ constraintList ret;
+ constraintList temp;
+ ret = constraintList_new();
+
+ ret = reflectChangesEnsures (list1, list2);
+ ret = constraintList_fixConflicts (ret, list2);
+ ret = constraintList_subsumeEnsures (ret, list2);
+ list2 = constraintList_subsumeEnsures (list2, ret);
+ temp = constraintList_copy(list2);
+
+ temp = constraintList_addList (temp, ret);
+ return temp;
+ //ret = constraintList_addList (ret, list2);
+ //return ret;
+}
+
void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
{
constraintList temp;
- TPRINTF( (message ("magically merging constraint into parent:%s for children: %s and %s", exprNode_unparse (parent), exprNode_unparse (child1), exprNode_unparse(child2) )
- ) );
- if (exprNode_isError (child1) || exprNode_isError(child2) )
+
+ TPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )));
+
+ TPRINTF( (message (" children: %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) );
+
+ if (exprNode_isError (child1) || exprNode_isError(child2) )
{
if (exprNode_isError (child1) && !exprNode_isError(child2) )
{
temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints);
parent->requiresConstraints = constraintList_addList (parent->requiresConstraints, temp);
-
- temp = reflectChangesEnsures (child1->ensuresConstraints, child2->ensuresConstraints);
- // temp = constraintList_copy (child1->ensuresConstraints);
-
- temp = constraintList_fixConflicts (temp, child2->ensuresConstraints);
-
- parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
- parent->ensuresConstraints = constraintList_addList (parent->ensuresConstraints, temp);
+ parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints,
+ child2->ensuresConstraints);
TPRINTF( (message ("Parent constraints are %s and %s ",
constraintList_print (parent->requiresConstraints),
+
+constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2)
+{
+ constraintList ret;
+ ret = constraintList_new();
+ constraintList_elements (list1, el)
+ {
+
+ TPRINTF ((message ("Examining %s", constraint_print (el) ) ) );
+ if (!resolve (el, list2) )
+ {
+ ret = constraintList_add (ret, el);
+ }
+ else
+ {
+ TPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) );
+ }
+ } end_constraintList_elements;
+
+ return ret;
+}
+
+
constraintList reflectChanges (constraintList pre2, constraintList post1)
{
if (!resolve (el, post1) )
{
temp = substitute (el, post1);
- ret = constraintList_add (ret, temp);
+ if (!resolve (temp, post1) )
+ ret = constraintList_add (ret, temp);
}
} end_constraintList_elements;
if (!resolve (el, post1) )
{
temp = substitute (el, post1);
- if (temp != NULL)
+ llassert (temp != NULL);
+
+ if (!resolve (temp, post1) )
ret = constraintList_add (ret, temp);
}
+ else
+ {
+ TPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) );
+ }
} end_constraintList_elements;
return ret;
if (constraintExpr_similar(c1->lexpr, c2->lexpr) )
{
- if (c1->ar == c2->ar)
- {
- TPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
- return TRUE;
- }
+ if (c1->ar == EQ)
+ if (c1->ar == c2->ar)
+ {
+ TPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
+ return TRUE;
+ }
}
- TPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
+ DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) );
return FALSE;
}
}
end_constraintList_elements;
- TPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
+ DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
return FALSE;
}
return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
}
+bool arithType_canResolve (arithType ar1, arithType ar2)
+{
+ switch (ar1)
+ {
+ case GTE:
+ case GT:
+ if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) )
+ {
+ return TRUE;
+ }
+ break;
+
+ case EQ:
+ if (ar2 == EQ)
+ return TRUE;
+ break;
+
+ case LT:
+ case LTE:
+ llassert(FALSE);
+ if ( (ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) )
+ return TRUE;
+ }
+ return FALSE;
+}
bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2)
{
- TPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));
+ DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));
+
+ if (! arithType_canResolve (ar1, ar2) )
+ return FALSE;
+
switch (ar1)
{
case GTE:
case GT:
- /*irst constraint is > only > => or == cosntraint can satify it */
- if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) )
- {
- if (! constraintExpr_canGetValue (expr1) )
- {
- TPRINTF( ("Can't Get value"));
- return FALSE;
- }
- if (! constraintExpr_canGetValue (expr2) )
- {
- TPRINTF( ("Can't Get value"));
- return FALSE;
- }
-
- if (constraintExpr_compare (expr2, expr1) >= 0)
- return TRUE;
-
- }
-
- return FALSE;
+ if (! (constraintExpr_canGetValue (expr1) &&
+ constraintExpr_canGetValue (expr2) ) )
+ {
+ DPRINTF( ("Can't Get value"));
+ return FALSE;
+ }
+
+ if (constraintExpr_compare (expr2, expr1) >= 0)
+ return TRUE;
+
+ return FALSE;
+ case EQ:
+ if (constraintExpr_similar (expr1, expr2) )
+ return TRUE;
+
+ return FALSE;
+
default:
- TPRINTF(("case not handled"));
+ DPRINTF(("case not handled"));
}
return FALSE;
}
+
constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new)
{
- TPRINTF (("Doing replace for lexpr") );
+ DPRINTF (("Doing replace for lexpr") );
c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, new);
- TPRINTF (("Doing replace for expr") );
+ DPRINTF (("Doing replace for expr") );
c->expr = constraintExpr_searchandreplace (c->expr, old, new);
return c;
}
+bool constraint_search (constraint c, constraintExpr old)
+{
+ bool ret;
+ ret = FALSE;
+
+ ret = constraintExpr_search (c->lexpr, old);
+ ret = ret || constraintExpr_search (c->expr, old);
+ return ret;
+}
+
constraint constraint_adjust (constraint substitute, constraint old)
{
fileloc loc1, loc2, loc3;
+ DPRINTF ( (message("Start adjust on %s and %s", constraint_print(substitute),
+ constraint_print(old))
+ ));
+
loc1 = constraint_getFileloc (old);
loc2 = constraintExpr_getFileloc (substitute->lexpr);
loc3 = constraintExpr_getFileloc (substitute->expr);
- if (fileloc_closer (loc1, loc3, loc2))
+
+ // special case of an equality that "contains itself"
+ if (constraintExpr_search (substitute->expr, substitute->lexpr) )
+ if (fileloc_closer (loc1, loc3, loc2))
{
constraintExpr temp;
+ DPRINTF ( (message("Doing adjust on %s", constraint_print(substitute) )
+ ));
temp = substitute->lexpr;
substitute->lexpr = substitute->expr;
substitute->expr = temp;
if (!constraint_conflict (c, el) )
{
-
constraint temp;
temp = constraint_copy(el);
temp = constraint_adjust(temp, c);
+
+ DPRINTF((message ("Substituting %s for %s",
+ constraint_print (temp), constraint_print (c)
+ ) ) );
+
- c = constraint_searchandreplace (c, el->lexpr, el->expr);
+ c = constraint_searchandreplace (c, temp->lexpr, temp->expr);
}
}
end_constraintList_elements;
constraint constraint_solve (constraint c)
{
- TPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) );
+ DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) );
c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr);
- TPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) );
+ DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) );
return c;
}
c->expr = constraintExpr_simplify (c->expr);
c = constraint_solve (c);
- /*
+
c->lexpr = constraintExpr_simplify (c->lexpr);
c->expr = constraintExpr_simplify (c->expr);
- */
+
return c;
}
return FALSE;
}
+
return FALSE;
}
- TPRINTF ( (message
+ DPRINTF ( (message
("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2)
)
)
}
else
{
- TPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) ));
+ DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) ));
return FALSE;
}
fileloc exprNode_getfileloc (exprNode p_e)
{
- return fileloc_copy ( p_e->loc );
+ if (p_e)
+ return fileloc_copy ( p_e->loc );
+ else
+ return fileloc_undefined;
}
fileloc exprNode_getNextSequencePoint (exprNode e)
lltok t = exprData_getUopTok (e->edata);
return lltok_getLoc (t);
} else {
- llcontbug (message ("Cannot get next sequence point: %s", exprNode_unparse (e)));
+ #warning fix
+ // llcontbug (message ("Cannot get next sequence point: %s", exprNode_unparse (e)));
return fileloc_undefined;
}
}
+
/* A Bison parser, made from llgrammar.y
- by GNU Bison version 1.25
- */
+ by GNU Bison version 1.28 */
#define YYBISON 1 /* Identify Bison output. */
#define yychar ylchar
#define yydebug yldebug
#define yynerrs ylnerrs
-#define simpleOp 258
-#define PREFIX_OP 259
-#define POSTFIX_OP 260
-#define LLT_MULOP 261
-#define LLT_SEMI 262
-#define LLT_VERTICALBAR 263
-#define ITERATION_OP 264
-#define LLT_LPAR 265
-#define LLT_LBRACKET 266
-#define selectSym 267
-#define LLT_IF_THEN_ELSE 268
-#define logicalOp 269
-#define eqSepSym 270
-#define equationSym 271
-#define commentSym 272
-#define LLT_WHITESPACE 273
-#define LLT_EOL 274
-#define LLT_TYPEDEF_NAME 275
-#define quantifierSym 276
-#define openSym 277
-#define closeSym 278
-#define sepSym 279
-#define simpleId 280
-#define mapSym 281
-#define markerSym 282
-#define preSym 283
-#define postSym 284
-#define anySym 285
-#define LLT_COLON 286
-#define LLT_COMMA 287
-#define LLT_EQUALS 288
-#define LLT_LBRACE 289
-#define LLT_RBRACE 290
-#define LLT_RBRACKET 291
-#define LLT_RPAR 292
-#define LLT_QUOTE 293
-#define eqOp 294
-#define LLT_CCHAR 295
-#define LLT_CFLOAT 296
-#define LLT_CINTEGER 297
-#define LLT_LCSTRING 298
-#define LLT_ALL 299
-#define LLT_ANYTHING 300
-#define LLT_BE 301
-#define LLT_BODY 302
-#define LLT_CLAIMS 303
-#define LLT_CHECKS 304
-#define LLT_CONSTANT 305
-#define LLT_ELSE 306
-#define LLT_ENSURES 307
-#define LLT_FOR 308
-#define LLT_FRESH 309
-#define LLT_IF 310
-#define LLT_IMMUTABLE 311
-#define LLT_IMPORTS 312
-#define LLT_CONSTRAINT 313
-#define LLT_ISSUB 314
-#define LLT_LET 315
-#define LLT_MODIFIES 316
-#define LLT_MUTABLE 317
-#define LLT_NOTHING 318
-#define LLT_INTERNAL 319
-#define LLT_FILESYS 320
-#define LLT_OBJ 321
-#define LLT_OUT 322
-#define LLT_SEF 323
-#define LLT_ONLY 324
-#define LLT_PARTIAL 325
-#define LLT_OWNED 326
-#define LLT_DEPENDENT 327
-#define LLT_KEEP 328
-#define LLT_KEPT 329
-#define LLT_TEMP 330
-#define LLT_SHARED 331
-#define LLT_UNIQUE 332
-#define LLT_UNUSED 333
-#define LLT_EXITS 334
-#define LLT_MAYEXIT 335
-#define LLT_NEVEREXIT 336
-#define LLT_TRUEEXIT 337
-#define LLT_FALSEEXIT 338
-#define LLT_UNDEF 339
-#define LLT_KILLED 340
-#define LLT_CHECKMOD 341
-#define LLT_CHECKED 342
-#define LLT_UNCHECKED 343
-#define LLT_CHECKEDSTRICT 344
-#define LLT_TRUENULL 345
-#define LLT_FALSENULL 346
-#define LLT_LNULL 347
-#define LLT_LNOTNULL 348
-#define LLT_RETURNED 349
-#define LLT_OBSERVER 350
-#define LLT_EXPOSED 351
-#define LLT_REFCOUNTED 352
-#define LLT_REFS 353
-#define LLT_RELNULL 354
-#define LLT_RELDEF 355
-#define LLT_KILLREF 356
-#define LLT_NULLTERMINATED 357
-#define LLT_TEMPREF 358
-#define LLT_NEWREF 359
-#define LLT_PRIVATE 360
-#define LLT_REQUIRES 361
-#define LLT_RESULT 362
-#define LLT_SIZEOF 363
-#define LLT_SPEC 364
-#define LLT_TAGGEDUNION 365
-#define LLT_THEN 366
-#define LLT_TYPE 367
-#define LLT_TYPEDEF 368
-#define LLT_UNCHANGED 369
-#define LLT_USES 370
-#define LLT_CHAR 371
-#define LLT_CONST 372
-#define LLT_DOUBLE 373
-#define LLT_ENUM 374
-#define LLT_FLOAT 375
-#define LLT_INT 376
-#define LLT_ITER 377
-#define LLT_YIELD 378
-#define LLT_LONG 379
-#define LLT_SHORT 380
-#define LLT_SIGNED 381
-#define LLT_UNKNOWN 382
-#define LLT_STRUCT 383
-#define LLT_TELIPSIS 384
-#define LLT_UNION 385
-#define LLT_UNSIGNED 386
-#define LLT_VOID 387
-#define LLT_VOLATILE 388
-#define LLT_PRINTFLIKE 389
-#define LLT_SCANFLIKE 390
-#define LLT_MESSAGELIKE 391
+#define simpleOp 257
+#define PREFIX_OP 258
+#define POSTFIX_OP 259
+#define LLT_MULOP 260
+#define LLT_SEMI 261
+#define LLT_VERTICALBAR 262
+#define ITERATION_OP 263
+#define LLT_LPAR 264
+#define LLT_LBRACKET 265
+#define selectSym 266
+#define LLT_IF_THEN_ELSE 267
+#define logicalOp 268
+#define eqSepSym 269
+#define equationSym 270
+#define commentSym 271
+#define LLT_WHITESPACE 272
+#define LLT_EOL 273
+#define LLT_TYPEDEF_NAME 274
+#define quantifierSym 275
+#define openSym 276
+#define closeSym 277
+#define sepSym 278
+#define simpleId 279
+#define mapSym 280
+#define markerSym 281
+#define preSym 282
+#define postSym 283
+#define anySym 284
+#define LLT_COLON 285
+#define LLT_COMMA 286
+#define LLT_EQUALS 287
+#define LLT_LBRACE 288
+#define LLT_RBRACE 289
+#define LLT_RBRACKET 290
+#define LLT_RPAR 291
+#define LLT_QUOTE 292
+#define eqOp 293
+#define LLT_CCHAR 294
+#define LLT_CFLOAT 295
+#define LLT_CINTEGER 296
+#define LLT_LCSTRING 297
+#define LLT_ALL 298
+#define LLT_ANYTHING 299
+#define LLT_BE 300
+#define LLT_BODY 301
+#define LLT_CLAIMS 302
+#define LLT_CHECKS 303
+#define LLT_CONSTANT 304
+#define LLT_ELSE 305
+#define LLT_ENSURES 306
+#define LLT_FOR 307
+#define LLT_FRESH 308
+#define LLT_IF 309
+#define LLT_IMMUTABLE 310
+#define LLT_IMPORTS 311
+#define LLT_CONSTRAINT 312
+#define LLT_ISSUB 313
+#define LLT_LET 314
+#define LLT_MODIFIES 315
+#define LLT_MUTABLE 316
+#define LLT_NOTHING 317
+#define LLT_INTERNAL 318
+#define LLT_FILESYS 319
+#define LLT_OBJ 320
+#define LLT_OUT 321
+#define LLT_SEF 322
+#define LLT_ONLY 323
+#define LLT_PARTIAL 324
+#define LLT_OWNED 325
+#define LLT_DEPENDENT 326
+#define LLT_KEEP 327
+#define LLT_KEPT 328
+#define LLT_TEMP 329
+#define LLT_SHARED 330
+#define LLT_UNIQUE 331
+#define LLT_UNUSED 332
+#define LLT_EXITS 333
+#define LLT_MAYEXIT 334
+#define LLT_NEVEREXIT 335
+#define LLT_TRUEEXIT 336
+#define LLT_FALSEEXIT 337
+#define LLT_UNDEF 338
+#define LLT_KILLED 339
+#define LLT_CHECKMOD 340
+#define LLT_CHECKED 341
+#define LLT_UNCHECKED 342
+#define LLT_CHECKEDSTRICT 343
+#define LLT_TRUENULL 344
+#define LLT_FALSENULL 345
+#define LLT_LNULL 346
+#define LLT_LNOTNULL 347
+#define LLT_RETURNED 348
+#define LLT_OBSERVER 349
+#define LLT_EXPOSED 350
+#define LLT_REFCOUNTED 351
+#define LLT_REFS 352
+#define LLT_RELNULL 353
+#define LLT_RELDEF 354
+#define LLT_KILLREF 355
+#define LLT_NULLTERMINATED 356
+#define LLT_TEMPREF 357
+#define LLT_NEWREF 358
+#define LLT_PRIVATE 359
+#define LLT_REQUIRES 360
+#define LLT_RESULT 361
+#define LLT_SIZEOF 362
+#define LLT_SPEC 363
+#define LLT_TAGGEDUNION 364
+#define LLT_THEN 365
+#define LLT_TYPE 366
+#define LLT_TYPEDEF 367
+#define LLT_UNCHANGED 368
+#define LLT_USES 369
+#define LLT_CHAR 370
+#define LLT_CONST 371
+#define LLT_DOUBLE 372
+#define LLT_ENUM 373
+#define LLT_FLOAT 374
+#define LLT_INT 375
+#define LLT_ITER 376
+#define LLT_YIELD 377
+#define LLT_LONG 378
+#define LLT_SHORT 379
+#define LLT_SIGNED 380
+#define LLT_UNKNOWN 381
+#define LLT_STRUCT 382
+#define LLT_TELIPSIS 383
+#define LLT_UNION 384
+#define LLT_UNSIGNED 385
+#define LLT_VOID 386
+#define LLT_VOLATILE 387
+#define LLT_PRINTFLIKE 388
+#define LLT_SCANFLIKE 389
+#define LLT_MESSAGELIKE 390
#line 36 "llgrammar.y"
#define YYFLAG -32768
#define YYNTBASE 137
-#define YYTRANSLATE(x) ((unsigned)(x) <= 391 ? yytranslate[x] : 291)
+#define YYTRANSLATE(x) ((unsigned)(x) <= 390 ? yytranslate[x] : 291)
static const short yytranslate[] = { 0,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 1, 2, 3, 4, 5,
- 6, 7, 8, 9, 10, 11, 12, 13, 14, 15,
- 16, 17, 18, 19, 20, 21, 22, 23, 24, 25,
- 26, 27, 28, 29, 30, 31, 32, 33, 34, 35,
- 36, 37, 38, 39, 40, 41, 42, 43, 44, 45,
- 46, 47, 48, 49, 50, 51, 52, 53, 54, 55,
- 56, 57, 58, 59, 60, 61, 62, 63, 64, 65,
- 66, 67, 68, 69, 70, 71, 72, 73, 74, 75,
- 76, 77, 78, 79, 80, 81, 82, 83, 84, 85,
- 86, 87, 88, 89, 90, 91, 92, 93, 94, 95,
- 96, 97, 98, 99, 100, 101, 102, 103, 104, 105,
- 106, 107, 108, 109, 110, 111, 112, 113, 114, 115,
- 116, 117, 118, 119, 120, 121, 122, 123, 124, 125,
- 126, 127, 128, 129, 130, 131, 132, 133, 134, 135,
- 136
+ 2, 2, 2, 2, 2, 1, 3, 4, 5, 6,
+ 7, 8, 9, 10, 11, 12, 13, 14, 15, 16,
+ 17, 18, 19, 20, 21, 22, 23, 24, 25, 26,
+ 27, 28, 29, 30, 31, 32, 33, 34, 35, 36,
+ 37, 38, 39, 40, 41, 42, 43, 44, 45, 46,
+ 47, 48, 49, 50, 51, 52, 53, 54, 55, 56,
+ 57, 58, 59, 60, 61, 62, 63, 64, 65, 66,
+ 67, 68, 69, 70, 71, 72, 73, 74, 75, 76,
+ 77, 78, 79, 80, 81, 82, 83, 84, 85, 86,
+ 87, 88, 89, 90, 91, 92, 93, 94, 95, 96,
+ 97, 98, 99, 100, 101, 102, 103, 104, 105, 106,
+ 107, 108, 109, 110, 111, 112, 113, 114, 115, 116,
+ 117, 118, 119, 120, 121, 122, 123, 124, 125, 126,
+ 127, 128, 129, 130, 131, 132, 133, 134, 135, 136
};
#if YYDEBUG != 0
-1, -1, 107, 108, -1, -1, -1, -1, -1, 114
};
/* -*-C-*- Note some compilers choke on comments on `#line' lines. */
-#line 3 "/usr/share/misc/bison.simple"
+#line 3 "/usr/lib/bison.simple"
+/* This file comes from bison-1.28. */
/* Skeleton output parser for bison,
Copyright (C) 1984, 1989, 1990 Free Software Foundation, Inc.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
- Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. */
+ Foundation, Inc., 59 Temple Place - Suite 330,
+ Boston, MA 02111-1307, USA. */
/* As a special exception, when this file is copied by Bison into a
Bison output file, you may use that output file without restriction.
This special exception was added by the Free Software Foundation
in version 1.24 of Bison. */
-#ifndef alloca
+/* This is the parser code that is written into each bison parser
+ when the %semantic_parser declaration is not specified in the grammar.
+ It was written by Richard Stallman by simplifying the hairy parser
+ used when %semantic_parser is specified. */
+
+#ifndef YYSTACK_USE_ALLOCA
+#ifdef alloca
+#define YYSTACK_USE_ALLOCA
+#else /* alloca not defined */
#ifdef __GNUC__
+#define YYSTACK_USE_ALLOCA
#define alloca __builtin_alloca
#else /* not GNU C. */
-#if (!defined (__STDC__) && defined (sparc)) || defined (__sparc__) || defined (__sparc) || defined (__sgi)
+#if (!defined (__STDC__) && defined (sparc)) || defined (__sparc__) || defined (__sparc) || defined (__sgi) || (defined (__sun) && defined (__i386))
+#define YYSTACK_USE_ALLOCA
#include <alloca.h>
#else /* not sparc */
-#if defined (MSDOS) && !defined (__TURBOC__)
+/* We think this test detects Watcom and Microsoft C. */
+/* This used to test MSDOS, but that is a bad idea
+ since that symbol is in the user namespace. */
+#if (defined (_MSDOS) || defined (_MSDOS_)) && !defined (__TURBOC__)
+#if 0 /* No need for malloc.h, which pollutes the namespace;
+ instead, just don't use alloca. */
#include <malloc.h>
+#endif
#else /* not MSDOS, or __TURBOC__ */
#if defined(_AIX)
-#include <malloc.h>
+/* I don't know what this was needed for, but it pollutes the namespace.
+ So I turned it off. rms, 2 May 1997. */
+/* #include <malloc.h> */
#pragma alloca
-#else /* not MSDOS, __TURBOC__, or _AIX */
-#ifdef __hpux
-#ifdef __cplusplus
-extern "C" {
-void *alloca (unsigned int);
-};
-#else /* not __cplusplus */
-void *alloca ();
-#endif /* not __cplusplus */
+#define YYSTACK_USE_ALLOCA
+#else /* not MSDOS, or __TURBOC__, or _AIX */
+#if 0
+#ifdef __hpux /* haible@ilog.fr says this works for HPUX 9.05 and up,
+ and on HPUX 10. Eventually we can turn this on. */
+#define YYSTACK_USE_ALLOCA
+#define alloca __builtin_alloca
#endif /* __hpux */
+#endif
#endif /* not _AIX */
#endif /* not MSDOS, or __TURBOC__ */
-#endif /* not sparc. */
-#endif /* not GNU C. */
-#endif /* alloca not defined. */
+#endif /* not sparc */
+#endif /* not GNU C */
+#endif /* alloca not defined */
+#endif /* YYSTACK_USE_ALLOCA not defined */
-/* This is the parser code that is written into each bison parser
- when the %semantic_parser declaration is not specified in the grammar.
- It was written by Richard Stallman by simplifying the hairy parser
- used when %semantic_parser is specified. */
+#ifdef YYSTACK_USE_ALLOCA
+#define YYSTACK_ALLOC alloca
+#else
+#define YYSTACK_ALLOC malloc
+#endif
/* Note: there must be only one dollar sign in this file.
It is replaced by the list of actions, each action
#define yyclearin (yychar = YYEMPTY)
#define YYEMPTY -2
#define YYEOF 0
-#define YYACCEPT return(0)
-#define YYABORT return(1)
+#define YYACCEPT goto yyacceptlab
+#define YYABORT goto yyabortlab
#define YYERROR goto yyerrlab1
/* Like YYERROR except do call yyerror.
This remains here temporarily to ease the
#ifndef YYMAXDEPTH
#define YYMAXDEPTH 10000
#endif
-
-/* Prevent warning if -Wstrict-prototypes. */
-#ifdef __GNUC__
-int yyparse (void);
-#endif
\f
+/* Define __yy_memcpy. Note that the size argument
+ should be passed with type unsigned int, because that is what the non-GCC
+ definitions require. With GCC, __builtin_memcpy takes an arg
+ of type size_t, but it can handle unsigned int. */
+
#if __GNUC__ > 1 /* GNU C and GNU C++ define this. */
#define __yy_memcpy(TO,FROM,COUNT) __builtin_memcpy(TO,FROM,COUNT)
#else /* not GNU C or C++ */
__yy_memcpy (to, from, count)
char *to;
char *from;
- int count;
+ unsigned int count;
{
register char *f = from;
register char *t = to;
/* This is the most reliable way to avoid incompatibilities
in available built-in functions on various systems. */
static void
-__yy_memcpy (char *to, char *from, int count)
+__yy_memcpy (char *to, char *from, unsigned int count)
{
- register char *f = from;
register char *t = to;
+ register char *f = from;
register int i = count;
while (i-- > 0)
#endif
#endif
\f
-#line 196 "/usr/share/misc/bison.simple"
+#line 217 "/usr/lib/bison.simple"
/* The user can define YYPARSE_PARAM as the name of an argument to be passed
into yyparse. The argument should have type void *.
#define YYPARSE_PARAM_DECL
#endif /* not YYPARSE_PARAM */
+/* Prevent warning if -Wstrict-prototypes. */
+#ifdef __GNUC__
+#ifdef YYPARSE_PARAM
+int yyparse (void *);
+#else
+int yyparse (void);
+#endif
+#endif
+
int
yyparse(YYPARSE_PARAM_ARG)
YYPARSE_PARAM_DECL
#endif
int yystacksize = YYINITDEPTH;
+ int yyfree_stacks = 0;
#ifdef YYPURE
int yychar;
if (yystacksize >= YYMAXDEPTH)
{
yyerror("parser stack overflow");
+ if (yyfree_stacks)
+ {
+ free (yyss);
+ free (yyvs);
+#ifdef YYLSP_NEEDED
+ free (yyls);
+#endif
+ }
return 2;
}
yystacksize *= 2;
if (yystacksize > YYMAXDEPTH)
yystacksize = YYMAXDEPTH;
- yyss = (short *) alloca (yystacksize * sizeof (*yyssp));
- __yy_memcpy ((char *)yyss, (char *)yyss1, size * sizeof (*yyssp));
- yyvs = (YYSTYPE *) alloca (yystacksize * sizeof (*yyvsp));
- __yy_memcpy ((char *)yyvs, (char *)yyvs1, size * sizeof (*yyvsp));
+#ifndef YYSTACK_USE_ALLOCA
+ yyfree_stacks = 1;
+#endif
+ yyss = (short *) YYSTACK_ALLOC (yystacksize * sizeof (*yyssp));
+ __yy_memcpy ((char *)yyss, (char *)yyss1,
+ size * (unsigned int) sizeof (*yyssp));
+ yyvs = (YYSTYPE *) YYSTACK_ALLOC (yystacksize * sizeof (*yyvsp));
+ __yy_memcpy ((char *)yyvs, (char *)yyvs1,
+ size * (unsigned int) sizeof (*yyvsp));
#ifdef YYLSP_NEEDED
- yyls = (YYLTYPE *) alloca (yystacksize * sizeof (*yylsp));
- __yy_memcpy ((char *)yyls, (char *)yyls1, size * sizeof (*yylsp));
+ yyls = (YYLTYPE *) YYSTACK_ALLOC (yystacksize * sizeof (*yylsp));
+ __yy_memcpy ((char *)yyls, (char *)yyls1,
+ size * (unsigned int) sizeof (*yylsp));
#endif
#endif /* no yyoverflow */
break;}
}
/* the action file gets copied in in place of this dollarsign */
-#line 498 "/usr/share/misc/bison.simple"
+#line 543 "/usr/lib/bison.simple"
\f
yyvsp -= yylen;
yyssp -= yylen;
yystate = yyn;
goto yynewstate;
+
+ yyacceptlab:
+ /* YYACCEPT comes here. */
+ if (yyfree_stacks)
+ {
+ free (yyss);
+ free (yyvs);
+#ifdef YYLSP_NEEDED
+ free (yyls);
+#endif
+ }
+ return 0;
+
+ yyabortlab:
+ /* YYABORT comes here. */
+ if (yyfree_stacks)
+ {
+ free (yyss);
+ free (yyvs);
+#ifdef YYLSP_NEEDED
+ free (yyls);
+#endif
+ }
+ return 1;
}
#line 1284 "llgrammar.y"
/* A Bison parser, made from llgrammar.y
- by GNU Bison version 1.25
- */
+ by GNU Bison version 1.28 */
#define YYBISON 1 /* Identify Bison output. */
#define yychar ylchar
#define yydebug yldebug
#define yynerrs ylnerrs
-#define simpleOp 258
-#define PREFIX_OP 259
-#define POSTFIX_OP 260
-#define LLT_MULOP 261
-#define LLT_SEMI 262
-#define LLT_VERTICALBAR 263
-#define ITERATION_OP 264
-#define LLT_LPAR 265
-#define LLT_LBRACKET 266
-#define selectSym 267
-#define LLT_IF_THEN_ELSE 268
-#define logicalOp 269
-#define eqSepSym 270
-#define equationSym 271
-#define commentSym 272
-#define LLT_WHITESPACE 273
-#define LLT_EOL 274
-#define LLT_TYPEDEF_NAME 275
-#define quantifierSym 276
-#define openSym 277
-#define closeSym 278
-#define sepSym 279
-#define simpleId 280
-#define mapSym 281
-#define markerSym 282
-#define preSym 283
-#define postSym 284
-#define anySym 285
-#define LLT_COLON 286
-#define LLT_COMMA 287
-#define LLT_EQUALS 288
-#define LLT_LBRACE 289
-#define LLT_RBRACE 290
-#define LLT_RBRACKET 291
-#define LLT_RPAR 292
-#define LLT_QUOTE 293
-#define eqOp 294
-#define LLT_CCHAR 295
-#define LLT_CFLOAT 296
-#define LLT_CINTEGER 297
-#define LLT_LCSTRING 298
-#define LLT_ALL 299
-#define LLT_ANYTHING 300
-#define LLT_BE 301
-#define LLT_BODY 302
-#define LLT_CLAIMS 303
-#define LLT_CHECKS 304
-#define LLT_CONSTANT 305
-#define LLT_ELSE 306
-#define LLT_ENSURES 307
-#define LLT_FOR 308
-#define LLT_FRESH 309
-#define LLT_IF 310
-#define LLT_IMMUTABLE 311
-#define LLT_IMPORTS 312
-#define LLT_CONSTRAINT 313
-#define LLT_ISSUB 314
-#define LLT_LET 315
-#define LLT_MODIFIES 316
-#define LLT_MUTABLE 317
-#define LLT_NOTHING 318
-#define LLT_INTERNAL 319
-#define LLT_FILESYS 320
-#define LLT_OBJ 321
-#define LLT_OUT 322
-#define LLT_SEF 323
-#define LLT_ONLY 324
-#define LLT_PARTIAL 325
-#define LLT_OWNED 326
-#define LLT_DEPENDENT 327
-#define LLT_KEEP 328
-#define LLT_KEPT 329
-#define LLT_TEMP 330
-#define LLT_SHARED 331
-#define LLT_UNIQUE 332
-#define LLT_UNUSED 333
-#define LLT_EXITS 334
-#define LLT_MAYEXIT 335
-#define LLT_NEVEREXIT 336
-#define LLT_TRUEEXIT 337
-#define LLT_FALSEEXIT 338
-#define LLT_UNDEF 339
-#define LLT_KILLED 340
-#define LLT_CHECKMOD 341
-#define LLT_CHECKED 342
-#define LLT_UNCHECKED 343
-#define LLT_CHECKEDSTRICT 344
-#define LLT_TRUENULL 345
-#define LLT_FALSENULL 346
-#define LLT_LNULL 347
-#define LLT_LNOTNULL 348
-#define LLT_RETURNED 349
-#define LLT_OBSERVER 350
-#define LLT_EXPOSED 351
-#define LLT_REFCOUNTED 352
-#define LLT_REFS 353
-#define LLT_RELNULL 354
-#define LLT_RELDEF 355
-#define LLT_KILLREF 356
-#define LLT_NULLTERMINATED 357
-#define LLT_TEMPREF 358
-#define LLT_NEWREF 359
-#define LLT_PRIVATE 360
-#define LLT_REQUIRES 361
-#define LLT_RESULT 362
-#define LLT_SIZEOF 363
-#define LLT_SPEC 364
-#define LLT_TAGGEDUNION 365
-#define LLT_THEN 366
-#define LLT_TYPE 367
-#define LLT_TYPEDEF 368
-#define LLT_UNCHANGED 369
-#define LLT_USES 370
-#define LLT_CHAR 371
-#define LLT_CONST 372
-#define LLT_DOUBLE 373
-#define LLT_ENUM 374
-#define LLT_FLOAT 375
-#define LLT_INT 376
-#define LLT_ITER 377
-#define LLT_YIELD 378
-#define LLT_LONG 379
-#define LLT_SHORT 380
-#define LLT_SIGNED 381
-#define LLT_UNKNOWN 382
-#define LLT_STRUCT 383
-#define LLT_TELIPSIS 384
-#define LLT_UNION 385
-#define LLT_UNSIGNED 386
-#define LLT_VOID 387
-#define LLT_VOLATILE 388
-#define LLT_PRINTFLIKE 389
-#define LLT_SCANFLIKE 390
-#define LLT_MESSAGELIKE 391
+#define simpleOp 257
+#define PREFIX_OP 258
+#define POSTFIX_OP 259
+#define LLT_MULOP 260
+#define LLT_SEMI 261
+#define LLT_VERTICALBAR 262
+#define ITERATION_OP 263
+#define LLT_LPAR 264
+#define LLT_LBRACKET 265
+#define selectSym 266
+#define LLT_IF_THEN_ELSE 267
+#define logicalOp 268
+#define eqSepSym 269
+#define equationSym 270
+#define commentSym 271
+#define LLT_WHITESPACE 272
+#define LLT_EOL 273
+#define LLT_TYPEDEF_NAME 274
+#define quantifierSym 275
+#define openSym 276
+#define closeSym 277
+#define sepSym 278
+#define simpleId 279
+#define mapSym 280
+#define markerSym 281
+#define preSym 282
+#define postSym 283
+#define anySym 284
+#define LLT_COLON 285
+#define LLT_COMMA 286
+#define LLT_EQUALS 287
+#define LLT_LBRACE 288
+#define LLT_RBRACE 289
+#define LLT_RBRACKET 290
+#define LLT_RPAR 291
+#define LLT_QUOTE 292
+#define eqOp 293
+#define LLT_CCHAR 294
+#define LLT_CFLOAT 295
+#define LLT_CINTEGER 296
+#define LLT_LCSTRING 297
+#define LLT_ALL 298
+#define LLT_ANYTHING 299
+#define LLT_BE 300
+#define LLT_BODY 301
+#define LLT_CLAIMS 302
+#define LLT_CHECKS 303
+#define LLT_CONSTANT 304
+#define LLT_ELSE 305
+#define LLT_ENSURES 306
+#define LLT_FOR 307
+#define LLT_FRESH 308
+#define LLT_IF 309
+#define LLT_IMMUTABLE 310
+#define LLT_IMPORTS 311
+#define LLT_CONSTRAINT 312
+#define LLT_ISSUB 313
+#define LLT_LET 314
+#define LLT_MODIFIES 315
+#define LLT_MUTABLE 316
+#define LLT_NOTHING 317
+#define LLT_INTERNAL 318
+#define LLT_FILESYS 319
+#define LLT_OBJ 320
+#define LLT_OUT 321
+#define LLT_SEF 322
+#define LLT_ONLY 323
+#define LLT_PARTIAL 324
+#define LLT_OWNED 325
+#define LLT_DEPENDENT 326
+#define LLT_KEEP 327
+#define LLT_KEPT 328
+#define LLT_TEMP 329
+#define LLT_SHARED 330
+#define LLT_UNIQUE 331
+#define LLT_UNUSED 332
+#define LLT_EXITS 333
+#define LLT_MAYEXIT 334
+#define LLT_NEVEREXIT 335
+#define LLT_TRUEEXIT 336
+#define LLT_FALSEEXIT 337
+#define LLT_UNDEF 338
+#define LLT_KILLED 339
+#define LLT_CHECKMOD 340
+#define LLT_CHECKED 341
+#define LLT_UNCHECKED 342
+#define LLT_CHECKEDSTRICT 343
+#define LLT_TRUENULL 344
+#define LLT_FALSENULL 345
+#define LLT_LNULL 346
+#define LLT_LNOTNULL 347
+#define LLT_RETURNED 348
+#define LLT_OBSERVER 349
+#define LLT_EXPOSED 350
+#define LLT_REFCOUNTED 351
+#define LLT_REFS 352
+#define LLT_RELNULL 353
+#define LLT_RELDEF 354
+#define LLT_KILLREF 355
+#define LLT_NULLTERMINATED 356
+#define LLT_TEMPREF 357
+#define LLT_NEWREF 358
+#define LLT_PRIVATE 359
+#define LLT_REQUIRES 360
+#define LLT_RESULT 361
+#define LLT_SIZEOF 362
+#define LLT_SPEC 363
+#define LLT_TAGGEDUNION 364
+#define LLT_THEN 365
+#define LLT_TYPE 366
+#define LLT_TYPEDEF 367
+#define LLT_UNCHANGED 368
+#define LLT_USES 369
+#define LLT_CHAR 370
+#define LLT_CONST 371
+#define LLT_DOUBLE 372
+#define LLT_ENUM 373
+#define LLT_FLOAT 374
+#define LLT_INT 375
+#define LLT_ITER 376
+#define LLT_YIELD 377
+#define LLT_LONG 378
+#define LLT_SHORT 379
+#define LLT_SIGNED 380
+#define LLT_UNKNOWN 381
+#define LLT_STRUCT 382
+#define LLT_TELIPSIS 383
+#define LLT_UNION 384
+#define LLT_UNSIGNED 385
+#define LLT_VOID 386
+#define LLT_VOLATILE 387
+#define LLT_PRINTFLIKE 388
+#define LLT_SCANFLIKE 389
+#define LLT_MESSAGELIKE 390
#line 36 "llgrammar.y"
#define YYFLAG -32768
#define YYNTBASE 137
-#define YYTRANSLATE(x) ((unsigned)(x) <= 391 ? yytranslate[x] : 291)
+#define YYTRANSLATE(x) ((unsigned)(x) <= 390 ? yytranslate[x] : 291)
static const short yytranslate[] = { 0,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
- 2, 2, 2, 2, 2, 1, 2, 3, 4, 5,
- 6, 7, 8, 9, 10, 11, 12, 13, 14, 15,
- 16, 17, 18, 19, 20, 21, 22, 23, 24, 25,
- 26, 27, 28, 29, 30, 31, 32, 33, 34, 35,
- 36, 37, 38, 39, 40, 41, 42, 43, 44, 45,
- 46, 47, 48, 49, 50, 51, 52, 53, 54, 55,
- 56, 57, 58, 59, 60, 61, 62, 63, 64, 65,
- 66, 67, 68, 69, 70, 71, 72, 73, 74, 75,
- 76, 77, 78, 79, 80, 81, 82, 83, 84, 85,
- 86, 87, 88, 89, 90, 91, 92, 93, 94, 95,
- 96, 97, 98, 99, 100, 101, 102, 103, 104, 105,
- 106, 107, 108, 109, 110, 111, 112, 113, 114, 115,
- 116, 117, 118, 119, 120, 121, 122, 123, 124, 125,
- 126, 127, 128, 129, 130, 131, 132, 133, 134, 135,
- 136
+ 2, 2, 2, 2, 2, 1, 3, 4, 5, 6,
+ 7, 8, 9, 10, 11, 12, 13, 14, 15, 16,
+ 17, 18, 19, 20, 21, 22, 23, 24, 25, 26,
+ 27, 28, 29, 30, 31, 32, 33, 34, 35, 36,
+ 37, 38, 39, 40, 41, 42, 43, 44, 45, 46,
+ 47, 48, 49, 50, 51, 52, 53, 54, 55, 56,
+ 57, 58, 59, 60, 61, 62, 63, 64, 65, 66,
+ 67, 68, 69, 70, 71, 72, 73, 74, 75, 76,
+ 77, 78, 79, 80, 81, 82, 83, 84, 85, 86,
+ 87, 88, 89, 90, 91, 92, 93, 94, 95, 96,
+ 97, 98, 99, 100, 101, 102, 103, 104, 105, 106,
+ 107, 108, 109, 110, 111, 112, 113, 114, 115, 116,
+ 117, 118, 119, 120, 121, 122, 123, 124, 125, 126,
+ 127, 128, 129, 130, 131, 132, 133, 134, 135, 136
};
#if YYDEBUG != 0
-1, -1, 107, 108, -1, -1, -1, -1, -1, 114
};
/* -*-C-*- Note some compilers choke on comments on `#line' lines. */
-#line 3 "/usr/share/misc/bison.simple"
+#line 3 "/usr/lib/bison.simple"
+/* This file comes from bison-1.28. */
/* Skeleton output parser for bison,
Copyright (C) 1984, 1989, 1990 Free Software Foundation, Inc.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
- Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. */
+ Foundation, Inc., 59 Temple Place - Suite 330,
+ Boston, MA 02111-1307, USA. */
/* As a special exception, when this file is copied by Bison into a
Bison output file, you may use that output file without restriction.
This special exception was added by the Free Software Foundation
in version 1.24 of Bison. */
-#ifndef alloca
+/* This is the parser code that is written into each bison parser
+ when the %semantic_parser declaration is not specified in the grammar.
+ It was written by Richard Stallman by simplifying the hairy parser
+ used when %semantic_parser is specified. */
+
+#ifndef YYSTACK_USE_ALLOCA
+#ifdef alloca
+#define YYSTACK_USE_ALLOCA
+#else /* alloca not defined */
#ifdef __GNUC__
+#define YYSTACK_USE_ALLOCA
#define alloca __builtin_alloca
#else /* not GNU C. */
-#if (!defined (__STDC__) && defined (sparc)) || defined (__sparc__) || defined (__sparc) || defined (__sgi)
+#if (!defined (__STDC__) && defined (sparc)) || defined (__sparc__) || defined (__sparc) || defined (__sgi) || (defined (__sun) && defined (__i386))
+#define YYSTACK_USE_ALLOCA
#include <alloca.h>
#else /* not sparc */
-#if defined (MSDOS) && !defined (__TURBOC__)
+/* We think this test detects Watcom and Microsoft C. */
+/* This used to test MSDOS, but that is a bad idea
+ since that symbol is in the user namespace. */
+#if (defined (_MSDOS) || defined (_MSDOS_)) && !defined (__TURBOC__)
+#if 0 /* No need for malloc.h, which pollutes the namespace;
+ instead, just don't use alloca. */
#include <malloc.h>
+#endif
#else /* not MSDOS, or __TURBOC__ */
#if defined(_AIX)
-#include <malloc.h>
+/* I don't know what this was needed for, but it pollutes the namespace.
+ So I turned it off. rms, 2 May 1997. */
+/* #include <malloc.h> */
#pragma alloca
-#else /* not MSDOS, __TURBOC__, or _AIX */
-#ifdef __hpux
-#ifdef __cplusplus
-extern "C" {
-void *alloca (unsigned int);
-};
-#else /* not __cplusplus */
-void *alloca ();
-#endif /* not __cplusplus */
+#define YYSTACK_USE_ALLOCA
+#else /* not MSDOS, or __TURBOC__, or _AIX */
+#if 0
+#ifdef __hpux /* haible@ilog.fr says this works for HPUX 9.05 and up,
+ and on HPUX 10. Eventually we can turn this on. */
+#define YYSTACK_USE_ALLOCA
+#define alloca __builtin_alloca
#endif /* __hpux */
+#endif
#endif /* not _AIX */
#endif /* not MSDOS, or __TURBOC__ */
-#endif /* not sparc. */
-#endif /* not GNU C. */
-#endif /* alloca not defined. */
+#endif /* not sparc */
+#endif /* not GNU C */
+#endif /* alloca not defined */
+#endif /* YYSTACK_USE_ALLOCA not defined */
-/* This is the parser code that is written into each bison parser
- when the %semantic_parser declaration is not specified in the grammar.
- It was written by Richard Stallman by simplifying the hairy parser
- used when %semantic_parser is specified. */
+#ifdef YYSTACK_USE_ALLOCA
+#define YYSTACK_ALLOC alloca
+#else
+#define YYSTACK_ALLOC malloc
+#endif
/* Note: there must be only one dollar sign in this file.
It is replaced by the list of actions, each action
#define yyclearin (yychar = YYEMPTY)
#define YYEMPTY -2
#define YYEOF 0
-#define YYACCEPT return(0)
-#define YYABORT return(1)
+#define YYACCEPT goto yyacceptlab
+#define YYABORT goto yyabortlab
#define YYERROR goto yyerrlab1
/* Like YYERROR except do call yyerror.
This remains here temporarily to ease the
#ifndef YYMAXDEPTH
#define YYMAXDEPTH 10000
#endif
-
-/* Prevent warning if -Wstrict-prototypes. */
-#ifdef __GNUC__
-int yyparse (void);
-#endif
\f
+/* Define __yy_memcpy. Note that the size argument
+ should be passed with type unsigned int, because that is what the non-GCC
+ definitions require. With GCC, __builtin_memcpy takes an arg
+ of type size_t, but it can handle unsigned int. */
+
#if __GNUC__ > 1 /* GNU C and GNU C++ define this. */
#define __yy_memcpy(TO,FROM,COUNT) __builtin_memcpy(TO,FROM,COUNT)
#else /* not GNU C or C++ */
__yy_memcpy (to, from, count)
char *to;
char *from;
- int count;
+ unsigned int count;
{
register char *f = from;
register char *t = to;
/* This is the most reliable way to avoid incompatibilities
in available built-in functions on various systems. */
static void
-__yy_memcpy (char *to, char *from, int count)
+__yy_memcpy (char *to, char *from, unsigned int count)
{
- register char *f = from;
register char *t = to;
+ register char *f = from;
register int i = count;
while (i-- > 0)
#endif
#endif
\f
-#line 196 "/usr/share/misc/bison.simple"
+#line 217 "/usr/lib/bison.simple"
/* The user can define YYPARSE_PARAM as the name of an argument to be passed
into yyparse. The argument should have type void *.
#define YYPARSE_PARAM_DECL
#endif /* not YYPARSE_PARAM */
+/* Prevent warning if -Wstrict-prototypes. */
+#ifdef __GNUC__
+#ifdef YYPARSE_PARAM
+int yyparse (void *);
+#else
+int yyparse (void);
+#endif
+#endif
+
int
yyparse(YYPARSE_PARAM_ARG)
YYPARSE_PARAM_DECL
#endif
int yystacksize = YYINITDEPTH;
+ int yyfree_stacks = 0;
#ifdef YYPURE
int yychar;
if (yystacksize >= YYMAXDEPTH)
{
yyerror("parser stack overflow");
+ if (yyfree_stacks)
+ {
+ free (yyss);
+ free (yyvs);
+#ifdef YYLSP_NEEDED
+ free (yyls);
+#endif
+ }
return 2;
}
yystacksize *= 2;
if (yystacksize > YYMAXDEPTH)
yystacksize = YYMAXDEPTH;
- yyss = (short *) alloca (yystacksize * sizeof (*yyssp));
- __yy_memcpy ((char *)yyss, (char *)yyss1, size * sizeof (*yyssp));
- yyvs = (YYSTYPE *) alloca (yystacksize * sizeof (*yyvsp));
- __yy_memcpy ((char *)yyvs, (char *)yyvs1, size * sizeof (*yyvsp));
+#ifndef YYSTACK_USE_ALLOCA
+ yyfree_stacks = 1;
+#endif
+ yyss = (short *) YYSTACK_ALLOC (yystacksize * sizeof (*yyssp));
+ __yy_memcpy ((char *)yyss, (char *)yyss1,
+ size * (unsigned int) sizeof (*yyssp));
+ yyvs = (YYSTYPE *) YYSTACK_ALLOC (yystacksize * sizeof (*yyvsp));
+ __yy_memcpy ((char *)yyvs, (char *)yyvs1,
+ size * (unsigned int) sizeof (*yyvsp));
#ifdef YYLSP_NEEDED
- yyls = (YYLTYPE *) alloca (yystacksize * sizeof (*yylsp));
- __yy_memcpy ((char *)yyls, (char *)yyls1, size * sizeof (*yylsp));
+ yyls = (YYLTYPE *) YYSTACK_ALLOC (yystacksize * sizeof (*yylsp));
+ __yy_memcpy ((char *)yyls, (char *)yyls1,
+ size * (unsigned int) sizeof (*yylsp));
#endif
#endif /* no yyoverflow */
break;}
}
/* the action file gets copied in in place of this dollarsign */
-#line 498 "/usr/share/misc/bison.simple"
+#line 543 "/usr/lib/bison.simple"
\f
yyvsp -= yylen;
yyssp -= yylen;
yystate = yyn;
goto yynewstate;
+
+ yyacceptlab:
+ /* YYACCEPT comes here. */
+ if (yyfree_stacks)
+ {
+ free (yyss);
+ free (yyvs);
+#ifdef YYLSP_NEEDED
+ free (yyls);
+#endif
+ }
+ return 0;
+
+ yyabortlab:
+ /* YYABORT comes here. */
+ if (yyfree_stacks)
+ {
+ free (yyss);
+ free (yyvs);
+#ifdef YYLSP_NEEDED
+ free (yyls);
+#endif
+ }
+ return 1;
}
#line 1284 "llgrammar.y"
/*@only@*/ interfaceNodeList interfacelist;
/*@only@*/ CTypesNode ctypes;
} YYSTYPE;
-#define simpleOp 258
-#define PREFIX_OP 259
-#define POSTFIX_OP 260
-#define LLT_MULOP 261
-#define LLT_SEMI 262
-#define LLT_VERTICALBAR 263
-#define ITERATION_OP 264
-#define LLT_LPAR 265
-#define LLT_LBRACKET 266
-#define selectSym 267
-#define LLT_IF_THEN_ELSE 268
-#define logicalOp 269
-#define eqSepSym 270
-#define equationSym 271
-#define commentSym 272
-#define LLT_WHITESPACE 273
-#define LLT_EOL 274
-#define LLT_TYPEDEF_NAME 275
-#define quantifierSym 276
-#define openSym 277
-#define closeSym 278
-#define sepSym 279
-#define simpleId 280
-#define mapSym 281
-#define markerSym 282
-#define preSym 283
-#define postSym 284
-#define anySym 285
-#define LLT_COLON 286
-#define LLT_COMMA 287
-#define LLT_EQUALS 288
-#define LLT_LBRACE 289
-#define LLT_RBRACE 290
-#define LLT_RBRACKET 291
-#define LLT_RPAR 292
-#define LLT_QUOTE 293
-#define eqOp 294
-#define LLT_CCHAR 295
-#define LLT_CFLOAT 296
-#define LLT_CINTEGER 297
-#define LLT_LCSTRING 298
-#define LLT_ALL 299
-#define LLT_ANYTHING 300
-#define LLT_BE 301
-#define LLT_BODY 302
-#define LLT_CLAIMS 303
-#define LLT_CHECKS 304
-#define LLT_CONSTANT 305
-#define LLT_ELSE 306
-#define LLT_ENSURES 307
-#define LLT_FOR 308
-#define LLT_FRESH 309
-#define LLT_IF 310
-#define LLT_IMMUTABLE 311
-#define LLT_IMPORTS 312
-#define LLT_CONSTRAINT 313
-#define LLT_ISSUB 314
-#define LLT_LET 315
-#define LLT_MODIFIES 316
-#define LLT_MUTABLE 317
-#define LLT_NOTHING 318
-#define LLT_INTERNAL 319
-#define LLT_FILESYS 320
-#define LLT_OBJ 321
-#define LLT_OUT 322
-#define LLT_SEF 323
-#define LLT_ONLY 324
-#define LLT_PARTIAL 325
-#define LLT_OWNED 326
-#define LLT_DEPENDENT 327
-#define LLT_KEEP 328
-#define LLT_KEPT 329
-#define LLT_TEMP 330
-#define LLT_SHARED 331
-#define LLT_UNIQUE 332
-#define LLT_UNUSED 333
-#define LLT_EXITS 334
-#define LLT_MAYEXIT 335
-#define LLT_NEVEREXIT 336
-#define LLT_TRUEEXIT 337
-#define LLT_FALSEEXIT 338
-#define LLT_UNDEF 339
-#define LLT_KILLED 340
-#define LLT_CHECKMOD 341
-#define LLT_CHECKED 342
-#define LLT_UNCHECKED 343
-#define LLT_CHECKEDSTRICT 344
-#define LLT_TRUENULL 345
-#define LLT_FALSENULL 346
-#define LLT_LNULL 347
-#define LLT_LNOTNULL 348
-#define LLT_RETURNED 349
-#define LLT_OBSERVER 350
-#define LLT_EXPOSED 351
-#define LLT_REFCOUNTED 352
-#define LLT_REFS 353
-#define LLT_RELNULL 354
-#define LLT_RELDEF 355
-#define LLT_KILLREF 356
-#define LLT_NULLTERMINATED 357
-#define LLT_TEMPREF 358
-#define LLT_NEWREF 359
-#define LLT_PRIVATE 360
-#define LLT_REQUIRES 361
-#define LLT_RESULT 362
-#define LLT_SIZEOF 363
-#define LLT_SPEC 364
-#define LLT_TAGGEDUNION 365
-#define LLT_THEN 366
-#define LLT_TYPE 367
-#define LLT_TYPEDEF 368
-#define LLT_UNCHANGED 369
-#define LLT_USES 370
-#define LLT_CHAR 371
-#define LLT_CONST 372
-#define LLT_DOUBLE 373
-#define LLT_ENUM 374
-#define LLT_FLOAT 375
-#define LLT_INT 376
-#define LLT_ITER 377
-#define LLT_YIELD 378
-#define LLT_LONG 379
-#define LLT_SHORT 380
-#define LLT_SIGNED 381
-#define LLT_UNKNOWN 382
-#define LLT_STRUCT 383
-#define LLT_TELIPSIS 384
-#define LLT_UNION 385
-#define LLT_UNSIGNED 386
-#define LLT_VOID 387
-#define LLT_VOLATILE 388
-#define LLT_PRINTFLIKE 389
-#define LLT_SCANFLIKE 390
-#define LLT_MESSAGELIKE 391
+#define simpleOp 257
+#define PREFIX_OP 258
+#define POSTFIX_OP 259
+#define LLT_MULOP 260
+#define LLT_SEMI 261
+#define LLT_VERTICALBAR 262
+#define ITERATION_OP 263
+#define LLT_LPAR 264
+#define LLT_LBRACKET 265
+#define selectSym 266
+#define LLT_IF_THEN_ELSE 267
+#define logicalOp 268
+#define eqSepSym 269
+#define equationSym 270
+#define commentSym 271
+#define LLT_WHITESPACE 272
+#define LLT_EOL 273
+#define LLT_TYPEDEF_NAME 274
+#define quantifierSym 275
+#define openSym 276
+#define closeSym 277
+#define sepSym 278
+#define simpleId 279
+#define mapSym 280
+#define markerSym 281
+#define preSym 282
+#define postSym 283
+#define anySym 284
+#define LLT_COLON 285
+#define LLT_COMMA 286
+#define LLT_EQUALS 287
+#define LLT_LBRACE 288
+#define LLT_RBRACE 289
+#define LLT_RBRACKET 290
+#define LLT_RPAR 291
+#define LLT_QUOTE 292
+#define eqOp 293
+#define LLT_CCHAR 294
+#define LLT_CFLOAT 295
+#define LLT_CINTEGER 296
+#define LLT_LCSTRING 297
+#define LLT_ALL 298
+#define LLT_ANYTHING 299
+#define LLT_BE 300
+#define LLT_BODY 301
+#define LLT_CLAIMS 302
+#define LLT_CHECKS 303
+#define LLT_CONSTANT 304
+#define LLT_ELSE 305
+#define LLT_ENSURES 306
+#define LLT_FOR 307
+#define LLT_FRESH 308
+#define LLT_IF 309
+#define LLT_IMMUTABLE 310
+#define LLT_IMPORTS 311
+#define LLT_CONSTRAINT 312
+#define LLT_ISSUB 313
+#define LLT_LET 314
+#define LLT_MODIFIES 315
+#define LLT_MUTABLE 316
+#define LLT_NOTHING 317
+#define LLT_INTERNAL 318
+#define LLT_FILESYS 319
+#define LLT_OBJ 320
+#define LLT_OUT 321
+#define LLT_SEF 322
+#define LLT_ONLY 323
+#define LLT_PARTIAL 324
+#define LLT_OWNED 325
+#define LLT_DEPENDENT 326
+#define LLT_KEEP 327
+#define LLT_KEPT 328
+#define LLT_TEMP 329
+#define LLT_SHARED 330
+#define LLT_UNIQUE 331
+#define LLT_UNUSED 332
+#define LLT_EXITS 333
+#define LLT_MAYEXIT 334
+#define LLT_NEVEREXIT 335
+#define LLT_TRUEEXIT 336
+#define LLT_FALSEEXIT 337
+#define LLT_UNDEF 338
+#define LLT_KILLED 339
+#define LLT_CHECKMOD 340
+#define LLT_CHECKED 341
+#define LLT_UNCHECKED 342
+#define LLT_CHECKEDSTRICT 343
+#define LLT_TRUENULL 344
+#define LLT_FALSENULL 345
+#define LLT_LNULL 346
+#define LLT_LNOTNULL 347
+#define LLT_RETURNED 348
+#define LLT_OBSERVER 349
+#define LLT_EXPOSED 350
+#define LLT_REFCOUNTED 351
+#define LLT_REFS 352
+#define LLT_RELNULL 353
+#define LLT_RELDEF 354
+#define LLT_KILLREF 355
+#define LLT_NULLTERMINATED 356
+#define LLT_TEMPREF 357
+#define LLT_NEWREF 358
+#define LLT_PRIVATE 359
+#define LLT_REQUIRES 360
+#define LLT_RESULT 361
+#define LLT_SIZEOF 362
+#define LLT_SPEC 363
+#define LLT_TAGGEDUNION 364
+#define LLT_THEN 365
+#define LLT_TYPE 366
+#define LLT_TYPEDEF 367
+#define LLT_UNCHANGED 368
+#define LLT_USES 369
+#define LLT_CHAR 370
+#define LLT_CONST 371
+#define LLT_DOUBLE 372
+#define LLT_ENUM 373
+#define LLT_FLOAT 374
+#define LLT_INT 375
+#define LLT_ITER 376
+#define LLT_YIELD 377
+#define LLT_LONG 378
+#define LLT_SHORT 379
+#define LLT_SIGNED 380
+#define LLT_UNKNOWN 381
+#define LLT_STRUCT 382
+#define LLT_TELIPSIS 383
+#define LLT_UNION 384
+#define LLT_UNSIGNED 385
+#define LLT_VOID 386
+#define LLT_VOLATILE 387
+#define LLT_PRINTFLIKE 388
+#define LLT_SCANFLIKE 389
+#define LLT_MESSAGELIKE 390
extern YYSTYPE yllval;
{
return (tok.tok == INC_OP);
}
+
+/* DRL added this function 10/23/2000 for boolean stuff */
+bool lltok_isEq_Op (lltok tok)
+{
+ return (tok.tok == EQ_OP);
+}
+
+/* DRL added this function 10/25/2000 for boolean stuff */
+bool lltok_isAnd_Op (lltok tok)
+{
+ return (tok.tok == AND_OP);
+}
+
+bool lltok_isOr_Op (lltok tok)
+{
+ return (tok.tok == OR_OP);
+}
+
+bool lltok_isNot_Op (lltok tok)
+{
+ return (tok.tok == TEXCL);
+}
+
cstring
lltok_unparse (lltok tok)
{
{
fileloc_free (t.loc);
}
+
andersk / splint.git / commitdiff
