1 /***** spin: pangen2.h *****/ 2 3 /* Copyright (c) 1989-2007 by Lucent Technologies, Bell Laboratories. */ 4 /* All Rights Reserved. This software is for educational purposes only. */ 5 /* No guarantee whatsoever is expressed or implied by the distribution of */ 6 /* this code. Permission is given to distribute this code provided that */ 7 /* this introductory message is not removed and no monies are exchanged. */ 8 /* Software written by Gerard J. Holzmann. For tool documentation see: */ 9 /* http://spinroot.com/ */ 10 /* Send all bug-reports and/or questions to: bugs@spinroot.com */ 11 /* (c) 2007: small additions for V5.0 to support multi-core verifications */ 12 13 static char *Pre0[] = { 14 "#ifdef SC", 15 "#define _FILE_OFFSET_BITS 64", /* to allow file sizes greater than 2Gb */ 16 "#endif", 17 "#include <stdio.h>", 18 "#include <signal.h>", 19 "#include <stdlib.h>", 20 "#include <stdarg.h>", 21 "#include <string.h>", 22 "#include <ctype.h>", 23 "#include <errno.h>", 24 "#if defined(WIN32) || defined(WIN64)", 25 "#include <time.h>", 26 "#else", 27 "#include <unistd.h>", 28 "#include <sys/times.h>", 29 "#endif", 30 "#include <sys/types.h>", /* defines off_t */ 31 "#include <sys/stat.h>", 32 "#include <fcntl.h>", 33 34 "#define Offsetof(X, Y) ((unsigned long)(&(((X *)0)->Y)))", 35 "#ifndef max", 36 "#define max(a,b) (((a)<(b)) ? (b) : (a))", 37 "#endif", 38 "#ifndef PRINTF", 39 "int Printf(const char *fmt, ...); /* prototype only */", 40 "#endif", 41 0, 42 }; 43 44 static char *Preamble[] = { 45 46 "#ifdef RANDOMIZE", 47 " #define T_RAND RANDOMIZE", 48 "#endif", 49 "#ifdef CNTRSTACK", 50 " #define onstack_now() (LL[trpt->j6] && LL[trpt->j7])", 51 " #define onstack_put() LL[trpt->j6]++; LL[trpt->j7]++", 52 " #define onstack_zap() LL[trpt->j6]--; LL[trpt->j7]--", 53 "#endif", 54 55 "#if !defined(SAFETY) && !defined(NOCOMP)", 56 /* 57 * V_A identifies states in the current statespace 58 * A_V identifies states in the 'other' statespace 59 * S_A remembers how many leading bytes in the sv 60 * are used for these markers + fairness bits 61 */ 62 " #define V_A (((now._a_t&1)?2:1) << (now._a_t&2))", 63 " #define A_V (((now._a_t&1)?1:2) << (now._a_t&2))", 64 " int S_A = 0;", 65 "#else", 66 " #define V_A 0", 67 " #define A_V 0", 68 " #define S_A 0", 69 "#endif", 70 71 "#ifdef MA", 72 "#undef onstack_now", 73 "#undef onstack_put", 74 "#undef onstack_zap", 75 "#define onstack_put() ;", 76 "#define onstack_zap() gstore((char *) &now, vsize, 4)", 77 "#else", 78 "#if defined(FULLSTACK) && !defined(BITSTATE)", 79 "#define onstack_put() trpt->ostate = Lstate", 80 "#define onstack_zap() { \\", 81 " if (trpt->ostate) \\", 82 " trpt->ostate->tagged = \\", 83 " (S_A)? (trpt->ostate->tagged&~V_A) : 0; \\", 84 " }", 85 "#endif", 86 "#endif", 87 88 "#ifndef NO_V_PROVISO", 89 "#define V_PROVISO", 90 "#endif", 91 "#if !defined(NO_RESIZE) && !defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(SPACE) && NCORE==1", 92 " #define AUTO_RESIZE", 93 "#endif", 94 "", 95 "struct H_el {", 96 " struct H_el *nxt;", 97 "#ifdef FULLSTACK", 98 " unsigned int tagged;", 99 " #if defined(BITSTATE) && !defined(NOREDUCE) && !defined(SAFETY)", 100 " unsigned int proviso;", /* uses just 1 bit 0/1 */ 101 " #endif", 102 "#endif", 103 "#if defined(CHECK) || (defined(COLLAPSE) && !defined(FULLSTACK))", 104 " unsigned long st_id;", 105 "#endif", 106 "#if !defined(SAFETY) || defined(REACH)", 107 " unsigned int D;", 108 "#endif", 109 "#ifdef BCS", 110 " #ifndef CONSERVATIVE", 111 " #define CONSERVATIVE 1 /* good for up to 8 processes */", 112 " #endif", 113 " #ifdef CONSERVATIVE", 114 " #if CONSERVATIVE <= 0 || CONSERVATIVE>32", 115 " #error sensible values for CONSERVATIVE are 1..32 (256/8 = 32)", 116 " #endif", 117 " uchar ctx_pid[CONSERVATIVE];", /* pids setting lowest value */ 118 " #endif", 119 " uchar ctx_low;", /* lowest nr of context switches seen so far */ 120 "#endif", 121 "#if NCORE>1", 122 " /* could cost 1 extra word: 4 bytes if 32-bit and 8 bytes if 64-bit */", 123 " #ifdef V_PROVISO", 124 " uchar cpu_id; /* id of cpu that created the state */", 125 " #endif", 126 "#endif", 127 "#ifdef COLLAPSE", 128 " #if VECTORSZ<65536", 129 " unsigned short ln;", /* length of vector */ 130 " #else", 131 " unsigned long ln;", /* length of vector */ 132 " #endif", 133 "#endif", 134 "#if defined(AUTO_RESIZE) && !defined(BITSTATE)", 135 " unsigned long m_K1;", 136 "#endif", 137 " unsigned long state;", 138 "} **H_tab, **S_Tab;\n", 139 140 "typedef struct Trail {", 141 " int st; /* current state */", 142 " int o_tt;", 143 " uchar pr; /* process id */", 144 " uchar tau; /* 8 bit-flags */", 145 " uchar o_pm; /* 8 more bit-flags */", 146 "#if 0", 147 " Meaning of bit-flags:", 148 " tau&1 -> timeout enabled", 149 " tau&2 -> request to enable timeout 1 level up (in claim)", 150 " tau&4 -> current transition is a claim move", 151 " tau&8 -> current transition is an atomic move", 152 " tau&16 -> last move was truncated on stack", 153 " tau&32 -> current transition is a preselected move", 154 " tau&64 -> at least one next state is not on the stack", 155 " tau&128 -> current transition is a stutter move", 156 157 " o_pm&1 -> the current pid moved -- implements else", 158 " o_pm&2 -> this is an acceptance state", 159 " o_pm&4 -> this is a progress state", 160 " o_pm&8 -> fairness alg rule 1 undo mark", 161 " o_pm&16 -> fairness alg rule 3 undo mark", 162 " o_pm&32 -> fairness alg rule 2 undo mark", 163 " o_pm&64 -> the current proc applied rule2", 164 " o_pm&128 -> a fairness, dummy move - all procs blocked", 165 "#endif", 166 "#ifdef NSUCC", 167 " uchar n_succ; /* nr of successor states */", 168 "#endif", 169 "#if defined(FULLSTACK) && defined(MA) && !defined(BFS)", 170 " uchar proviso;", 171 "#endif", 172 "#ifndef BFS", 173 " uchar o_n, o_ot; /* to save locals */", 174 "#endif", 175 " uchar o_m;", 176 "#ifdef EVENT_TRACE", 177 " #if nstates_event<256", 178 " uchar o_event;", 179 " #else", 180 " unsigned short o_event;", 181 " #endif", 182 "#endif", 183 "#ifndef BFS", 184 " short o_To;", 185 " #ifdef T_RAND", 186 " short oo_i;", 187 " #endif", 188 "#endif", 189 "#if defined(HAS_UNLESS) && !defined(BFS)", 190 " int e_state; /* if escape trans - state of origin */", 191 "#endif", 192 "#if (defined(FULLSTACK) && !defined(MA)) || defined(BFS) || (NCORE>1)", 193 " struct H_el *ostate; /* pointer to stored state */", 194 "#endif", 195 /* CNTRSTACK when !NOREDUCE && BITSTATE && SAFETY, uses LL[] */ 196 "#if defined(CNTRSTACK) && !defined(BFS)", 197 " long j6, j7;", 198 "#endif", 199 " Trans *o_t;", /* transition fct, next state */ 200 201 "#if !defined(BFS) && !defined(TRIX_ORIG)", 202 " char *p_bup;", 203 " char *q_bup;", 204 "#endif", 205 206 "#ifdef BCS", 207 " unsigned short sched_limit;", 208 " unsigned char bcs; /* phase 1 or 2, or forced 4 */", 209 " unsigned char b_pno; /* preferred pid */", 210 "#endif", 211 212 "#ifdef P_RAND", /* process scheduling randomization */ 213 " unsigned char p_left; /* nr of procs left to explore */", 214 " short p_skip; /* to find starting point in list */", 215 "#endif", 216 217 "#ifdef HAS_SORTED", 218 " short ipt;", /* insertion slot in q */ 219 "#endif", 220 " union {", 221 " int oval;", /* single backup value of variable */ 222 " int *ovals;", /* ptr to multiple values */ 223 " } bup;", 224 "} Trail;", 225 "Trail *trail, *trpt;", 226 227 "FILE *efd;", 228 "uchar *this;", 229 "long maxdepth=10000;", 230 "long omaxdepth=10000;", 231 "#ifdef BCS", 232 " /* bitflags in trpt->bcs */", 233 " #define B_PHASE1 1", 234 " #define B_PHASE2 2", 235 " #define B_FORCED 4", 236 "int sched_max = 0;", 237 "#endif", 238 "#ifdef PERMUTED", 239 " uchar permuted = 1;", 240 "#else", 241 " uchar permuted = 0;", 242 "#endif", 243 "double quota; /* time limit */", 244 "#if NCORE>1", 245 "long z_handoff = -1;", 246 "#endif", 247 "#ifdef SC", /* stack cycling */ 248 "char *stackfile;", 249 "#endif", 250 "uchar *SS, *LL;", 251 "uchar HASH_NR = 0;", 252 "", 253 "double memcnt = (double) 0;", 254 "double memlim = (double) (1<<30); /* 1 GB */", 255 "#if NCORE>1", 256 "double mem_reserved = (double) 0;", 257 "#endif", 258 "", 259 "/* for emalloc: */", 260 "static char *have;", 261 "static long left = 0L;", 262 "static double fragment = (double) 0;", 263 "static unsigned long grow;", 264 "", 265 #if 1 266 "unsigned int HASH_CONST[] = {", 267 " /* asuming 4 bytes per int */", 268 " 0x100d4e63, 0x0fc22f87,", 269 " 0x3ff0c3ff, 0x38e84cd7,", 270 " 0x02b148e9, 0x98b2e49d,", 271 " 0xb616d379, 0xa5247fd9,", 272 " 0xbae92a15, 0xb91c8bc5,", 273 " 0x8e5880f3, 0xacd7c069,", 274 " 0xb4c44bb3, 0x2ead1fb7,", 275 " 0x8e428171, 0xdbebd459,", 276 " 0x00400007, 0x04c11db7,", 277 " 0x828ae611, 0x6cb25933,", 278 " 0x86cdd651, 0x9e8f5f21,", 279 " 0xd5f8d8e7, 0x9c4e956f,", 280 " 0xb5cf2c71, 0x2e805a6d,", 281 " 0x33fc3a55, 0xaf203ed1,", 282 " 0xe31f5909, 0x5276db35,", 283 " 0x0c565ef7, 0x273d1aa5,", 284 " 0x8923b1dd, 0xa9acaac5,", 285 " 0xd1f69207, 0xedfd944b,", 286 " 0x9a68e46b, 0x5355e13f,", 287 " 0x7eeb44f9, 0x932beea9,", 288 " 0x330c4cd3, 0x87f34e5f,", 289 " 0x1b5851b7, 0xb9ca6447,", 290 " 0x58f96a8f, 0x1b3b5307,", 291 " 0x31c387b3, 0xf35f0f35,", 292 " 0xa0acc4df, 0xf3140303,", 293 " 0x2446245d, 0xe4b8f4ef,", 294 " 0x5c007383, 0x68e648af,", 295 " 0x1814fba7, 0xcdf731b5,", 296 " 0xd09ccb4b, 0xb92d0eff,", 297 " 0xcc3c6b67, 0xd3af6a57,", 298 " 0xf44fc3f5, 0x5bb67623,", 299 " 0xaeb9c953, 0x5e0ac739,", 300 " 0x3a7fda09, 0x5edf39eb,", 301 " 0x661eefd9, 0x6423f0d1,", 302 " 0x910fe413, 0x9ec92297,", 303 " 0x4bd8159d, 0xa7b16ee1,", 304 " 0x89d484e9, 0x7f305cb3,", 305 " 0xc5f303e7, 0x415deeef,", 306 " 0x09986f89, 0x7e9c4117,", 307 " 0x0b7cbedb, 0xf9ed7561,", 308 " 0x7a20ac99, 0xf05adef3,", 309 " 0x5893d75b, 0x44d73327,", 310 " 0xb583c873, 0x324d2145,", 311 " 0x7fa3829b, 0xe4b47a23,", 312 " 0xe256d94f, 0xb1fd8959,", 313 " 0xe561a321, 0x1435ac09,", 314 " 0xdd62408b, 0x02ec0bcb,", 315 " 0x5469b785, 0x2f4f50bb,", 316 " 0x20f19395, 0xf96ba085,", 317 " 0x2381f937, 0x768e2a11,", 318 " 0", 319 "};", 320 #else 321 "unsigned int HASH_CONST[] = {", 322 " /* asuming 4 bytes per int */", 323 " 0x88888EEF, 0x00400007,", 324 " 0x04c11db7, 0x100d4e63,", 325 " 0x0fc22f87, 0x3ff0c3ff,", 326 " 0x38e84cd7, 0x02b148e9,", 327 " 0x98b2e49d, 0xb616d379,", 328 " 0xa5247fd9, 0xbae92a15,", 329 " 0xb91c8bc5, 0x8e5880f3,", 330 " 0xacd7c069, 0xb4c44bb3,", 331 " 0x2ead1fb7, 0x8e428171,", 332 " 0xdbebd459, 0x828ae611,", 333 " 0x6cb25933, 0x86cdd651,", 334 " 0x9e8f5f21, 0xd5f8d8e7,", 335 " 0x9c4e956f, 0xb5cf2c71,", 336 " 0x2e805a6d, 0x33fc3a55,", 337 " 0xaf203ed1, 0xe31f5909,", 338 " 0x5276db35, 0x0c565ef7,", 339 " 0x273d1aa5, 0x8923b1dd,", 340 " 0", 341 "};", 342 #endif 343 "#if NCORE>1", 344 "extern int core_id;", 345 "#endif", 346 "long mreached=0;", 347 "int done=0, errors=0, Nrun=1;", 348 "int c_init_done=0;", 349 "char *c_stack_start = (char *) 0;", 350 "double nstates=0, nlinks=0, truncs=0, truncs2=0;", 351 "double nlost=0, nShadow=0, hcmp=0, ngrabs=0;", 352 "#ifdef PUTPID", 353 "char *progname;", 354 "#endif", 355 "#if defined(ZAPH) && defined(BITSTATE)", 356 "double zstates = 0;", 357 "#endif", 358 "int c_init_run;", 359 "#ifdef BFS", 360 "double midrv=0, failedrv=0, revrv=0;", 361 "#endif", 362 "unsigned long nr_states=0; /* nodes in DFA */", 363 "long Fa=0, Fh=0, Zh=0, Zn=0;", 364 "long PUT=0, PROBE=0, ZAPS=0;", 365 "long Ccheck=0, Cholds=0;", 366 "int a_cycles=0, upto=1, strict=0, verbose = 0, signoff = 0;", 367 "#ifdef HAS_CODE", 368 "int gui = 0, coltrace = 0, readtrail = 0;", 369 "int whichtrail = 0, whichclaim = -1, onlyproc = -1, silent = 0;", 370 "char *claimname;", 371 "#endif", 372 "int state_tables=0, fairness=0, no_rck=0, Nr_Trails=0, dodot=0;", 373 "char simvals[128];", 374 "#ifndef INLINE", 375 "int TstOnly=0;", 376 "#endif", 377 "unsigned long mask, nmask;", 378 "#ifdef BITSTATE", 379 "int ssize=23; /* 1 Mb */", 380 "#else", 381 "int ssize=19; /* 512K slots */", 382 "#endif", 383 "int hmax=0, svmax=0, smax=0;", 384 "int Maxbody=0, XX;", 385 "uchar *noptr, *noqptr; /* used by Pptr(x) and Qptr(x) */", 386 "#ifdef VAR_RANGES", 387 "void logval(char *, int);", 388 "void dumpranges(void);", 389 "#endif", 390 391 "#ifdef MA", 392 "#define INLINE_REV", 393 "extern void dfa_init(unsigned short);", 394 "extern int dfa_member(unsigned long);", 395 "extern int dfa_store(uchar *);", 396 "unsigned int maxgs = 0;", 397 "#endif", 398 "", 399 "#ifdef ALIGNED", 400 " State comp_now __attribute__ ((aligned (8)));", 401 " /* gcc 64-bit aligned for Itanium2 systems */", 402 " /* MAJOR runtime penalty if not used on those systems */", 403 "#else", 404 " State comp_now; /* compressed state vector */", 405 "#endif", 406 "", 407 "State comp_msk;", 408 "uchar *Mask = (uchar *) &comp_msk;", 409 "#ifdef COLLAPSE", 410 "State comp_tmp;", 411 "static char *scratch = (char *) &comp_tmp;", 412 "#endif", 413 414 "_Stack *stack; /* for queues, processes */", 415 "Svtack *svtack; /* for old state vectors */", 416 "#ifdef BITSTATE", 417 "static unsigned int hfns = 3; /* new default */", 418 "#endif", 419 "static unsigned long j1_spin; /* 5.2.1: avoid nameclash with math.h */", 420 "static unsigned long K1, K2;", 421 "static unsigned long j2, j3, j4;", 422 "#ifdef BITSTATE", 423 "static long udmem;", 424 "#endif", 425 "static long A_depth = 0;", 426 "long depth = 0;", 427 /* depth: not static to support -S2, but possible clash with embedded code */ 428 "#if NCORE>1", 429 "long nr_handoffs = 0;", 430 "#endif", 431 "static uchar warned = 0, iterative = 0, exclusive = 0, like_java = 0, every_error = 0;", 432 "static uchar noasserts = 0, noends = 0, bounded = 0;", 433 434 "#if defined(T_RAND) || defined(P_RAND) || defined(RANDSTOR)", 435 "unsigned int s_rand = 123; /* default seed */", 436 "#endif", 437 438 "#if SYNC>0 && ASYNC==0", 439 "void set_recvs(void);", 440 "int no_recvs(int);", 441 "#endif", 442 "#if SYNC", 443 "#define IfNotBlocked if (boq != -1) continue;", 444 "#define UnBlock boq = -1", 445 "#else", 446 "#define IfNotBlocked /* cannot block */", 447 "#define UnBlock /* don't bother */", 448 "#endif\n", 449 "#ifdef BITSTATE", 450 "int (*bstore)(char *, int);", 451 "int bstore_reg(char *, int);", 452 "int bstore_mod(char *, int);", 453 "#endif", 454 "void active_procs(void);", 455 "void cleanup(void);", 456 "void do_the_search(void);", 457 "void find_shorter(int);", 458 "void iniglobals(int);", 459 "void stopped(int);", 460 "void wrapup(void);", 461 "int *grab_ints(int);", 462 "void ungrab_ints(int *, int);", 463 0, 464 }; 465 466 static char *Tail[] = { 467 "Trans *", 468 "settr( int t_id, int a, int b, int c, int d,", 469 " char *t, int g, int tpe0, int tpe1)", 470 "{ Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n", 471 " tmp->atom = a&(6|32); /* only (2|8|32) have meaning */", 472 " if (!g) tmp->atom |= 8; /* no global references */", 473 " tmp->st = b;", 474 " tmp->tpe[0] = tpe0;", 475 " tmp->tpe[1] = tpe1;", 476 " tmp->tp = t;", 477 " tmp->t_id = t_id;", 478 " tmp->forw = c;", 479 " tmp->back = d;", 480 " return tmp;", 481 "}\n", 482 "Trans *", 483 "cpytr(Trans *a)", 484 "{ Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n", 485 " int i;", 486 " tmp->atom = a->atom;", 487 " tmp->st = a->st;", 488 "#ifdef HAS_UNLESS", 489 " tmp->e_trans = a->e_trans;", 490 " for (i = 0; i < HAS_UNLESS; i++)", 491 " tmp->escp[i] = a->escp[i];", 492 "#endif", 493 " tmp->tpe[0] = a->tpe[0];", 494 " tmp->tpe[1] = a->tpe[1];", 495 " for (i = 0; i < 6; i++)", 496 " { tmp->qu[i] = a->qu[i];", 497 " tmp->ty[i] = a->ty[i];", 498 " }", 499 " tmp->tp = (char *) emalloc(strlen(a->tp)+1);", 500 " strcpy(tmp->tp, a->tp);", 501 " tmp->t_id = a->t_id;", 502 " tmp->forw = a->forw;", 503 " tmp->back = a->back;", 504 " return tmp;", 505 "}\n", 506 "#ifndef NOREDUCE", 507 "int", 508 "srinc_set(int n)", 509 "{ if (n <= 2) return LOCAL;", 510 " if (n <= 2+ DELTA) return Q_FULL_F; /* 's' or nfull */", 511 " if (n <= 2+2*DELTA) return Q_EMPT_F; /* 'r' or nempty */", 512 " if (n <= 2+3*DELTA) return Q_EMPT_T; /* empty */", 513 " if (n <= 2+4*DELTA) return Q_FULL_T; /* full */", 514 " if (n == 5*DELTA) return GLOBAL;", 515 " if (n == 6*DELTA) return TIMEOUT_F;", 516 " if (n == 7*DELTA) return ALPHA_F;", 517 " Uerror(\"cannot happen srinc_class\");", 518 " return BAD;", 519 "}", 520 "int", 521 "srunc(int n, int m)", 522 "{ switch(m) {", 523 " case Q_FULL_F: return n-2;", 524 " case Q_EMPT_F: return n-2-DELTA;", 525 " case Q_EMPT_T: return n-2-2*DELTA;", 526 " case Q_FULL_T: return n-2-3*DELTA;", 527 " case ALPHA_F:", 528 " case TIMEOUT_F: return 257; /* non-zero, and > MAXQ */", 529 " }", 530 " Uerror(\"cannot happen srunc\");", 531 " return 0;", 532 "}", 533 "#endif", 534 "int cnt;", 535 "#ifdef HAS_UNLESS", 536 "int", 537 "isthere(Trans *a, int b)", /* is b already in a's list? */ 538 "{ Trans *t;", 539 " for (t = a; t; t = t->nxt)", 540 " if (t->t_id == b)", 541 " return 1;", 542 " return 0;", 543 "}", 544 "#endif", 545 "#ifndef NOREDUCE", 546 "int", 547 "mark_safety(Trans *t) /* for conditional safety */", 548 "{ int g = 0, i, j, k;", 549 "", 550 " if (!t) return 0;", 551 " if (t->qu[0])", 552 " return (t->qu[1])?2:1; /* marked */", 553 "", 554 " for (i = 0; i < 2; i++)", 555 " { j = srinc_set(t->tpe[i]);", 556 " if (j >= GLOBAL && j != ALPHA_F)", 557 " return -1;", 558 " if (j != LOCAL)", 559 " { k = srunc(t->tpe[i], j);", 560 " if (g == 0", 561 " || t->qu[0] != k", 562 " || t->ty[0] != j)", 563 " { t->qu[g] = k;", 564 " t->ty[g] = j;", 565 " g++;", 566 " } } }", 567 " return g;", 568 "}", 569 "#endif", 570 "void", 571 "retrans(int n, int m, int is, short srcln[], uchar reach[], uchar lstate[])", 572 " /* process n, with m states, is=initial state */", 573 "{ Trans *T0, *T1, *T2, *T3, *T4, *T5;", 574 " int i, k;", 575 "#ifndef NOREDUCE", 576 " int g, h, j, aa;", 577 "#endif", 578 "#ifdef HAS_UNLESS", 579 " int p;", 580 "#endif", 581 " if (state_tables >= 4)", 582 " { printf(\"STEP 1 %%s\\n\", ", 583 " procname[n]);", 584 " for (i = 1; i < m; i++)", 585 " for (T0 = trans[n][i]; T0; T0 = T0->nxt)", 586 " crack(n, i, T0, srcln);", 587 " return;", 588 " }", 589 " do {", 590 " for (i = 1, cnt = 0; i < m; i++)", 591 " { T2 = trans[n][i];", 592 " T1 = T2?T2->nxt:(Trans *)0;", 593 "/* prescan: */ for (T0 = T1; T0; T0 = T0->nxt)", 594 "/* choice in choice */ { if (T0->st && trans[n][T0->st]", 595 " && trans[n][T0->st]->nxt)", 596 " break;", 597 " }", 598 "#if 0", 599 " if (T0)", 600 " printf(\"\\tstate %%d / %%d: choice in choice\\n\",", 601 " i, T0->st);", 602 "#endif", 603 " if (T0)", 604 " for (T0 = T1; T0; T0 = T0->nxt)", 605 " { T3 = trans[n][T0->st];", 606 " if (!T3->nxt)", 607 " { T2->nxt = cpytr(T0);", 608 " T2 = T2->nxt;", 609 " imed(T2, T0->st, n, i);", 610 " continue;", 611 " }", 612 " do { T3 = T3->nxt;", 613 " T2->nxt = cpytr(T3);", 614 " T2 = T2->nxt;", 615 " imed(T2, T0->st, n, i);", 616 " } while (T3->nxt);", 617 " cnt++;", 618 " }", 619 " }", 620 " } while (cnt);", 621 622 " if (state_tables >= 3)", 623 " { printf(\"STEP 2 %%s\\n\", ", 624 " procname[n]);", 625 " for (i = 1; i < m; i++)", 626 " for (T0 = trans[n][i]; T0; T0 = T0->nxt)", 627 " crack(n, i, T0, srcln);", 628 " return;", 629 " }", 630 " for (i = 1; i < m; i++)", 631 " { if (trans[n][i] && trans[n][i]->nxt) /* optimize */", 632 " { T1 = trans[n][i]->nxt;", 633 "#if 0", 634 " printf(\"\\t\\tpull %%d (%%d) to %%d\\n\",", 635 " T1->st, T1->forw, i);", 636 "#endif", /* pull linenumber ref as well: */ 637 " srcln[i] = srcln[T1->st]; /* Oyvind Teig, 5.2.0 */", 638 "", 639 " if (!trans[n][T1->st]) continue;", 640 " T0 = cpytr(trans[n][T1->st]);", 641 " trans[n][i] = T0;", 642 " reach[T1->st] = 1;", 643 " imed(T0, T1->st, n, i);", 644 " for (T1 = T1->nxt; T1; T1 = T1->nxt)", 645 " {", 646 "#if 0", 647 " printf(\"\\t\\tpull %%d (%%d) to %%d\\n\",", 648 " T1->st, T1->forw, i);", 649 "#endif", 650 " /* srcln[i] = srcln[T1->st]; gh: not useful */", 651 " if (!trans[n][T1->st]) continue;", 652 " T0->nxt = cpytr(trans[n][T1->st]);", 653 " T0 = T0->nxt;", 654 " reach[T1->st] = 1;", 655 " imed(T0, T1->st, n, i);", 656 " } } }", 657 " if (state_tables >= 2)", 658 " { printf(\"STEP 3 %%s\\n\", ", 659 " procname[n]);", 660 " for (i = 1; i < m; i++)", 661 " for (T0 = trans[n][i]; T0; T0 = T0->nxt)", 662 " crack(n, i, T0, srcln);", 663 " return;", 664 " }", 665 "#ifdef HAS_UNLESS", 666 " for (i = 1; i < m; i++)", 667 " { if (!trans[n][i]) continue;", 668 " /* check for each state i if an", 669 " * escape to some state p is defined", 670 " * if so, copy and mark p's transitions", 671 " * and prepend them to the transition-", 672 " * list of state i", 673 " */", 674 " if (!like_java) /* the default */", 675 " { for (T0 = trans[n][i]; T0; T0 = T0->nxt)", 676 " for (k = HAS_UNLESS-1; k >= 0; k--)", 677 " { if (p = T0->escp[k])", 678 " for (T1 = trans[n][p]; T1; T1 = T1->nxt)", 679 " { if (isthere(trans[n][i], T1->t_id))", 680 " continue;", 681 " T2 = cpytr(T1);", 682 " T2->e_trans = p;", 683 " T2->nxt = trans[n][i];", 684 " trans[n][i] = T2;", 685 " } }", 686 " } else /* outermost unless checked first */", 687 " { T4 = T3 = (Trans *) 0;", 688 " for (T0 = trans[n][i]; T0; T0 = T0->nxt)", 689 " for (k = HAS_UNLESS-1; k >= 0; k--)", 690 " { if (p = T0->escp[k])", 691 " for (T1 = trans[n][p]; T1; T1 = T1->nxt)", 692 " { if (isthere(trans[n][i], T1->t_id))", 693 " continue;", 694 " T2 = cpytr(T1);", 695 " T2->nxt = (Trans *) 0;", 696 " T2->e_trans = p;", 697 " if (T3) T3->nxt = T2;", 698 " else T4 = T2;", 699 " T3 = T2;", 700 " } }", 701 " if (T4)", 702 " { T3->nxt = trans[n][i];", 703 " trans[n][i] = T4;", 704 " }", 705 " }", 706 " }", 707 "#endif", 708 709 "#ifndef NOREDUCE", 710 " for (i = 1; i < m; i++)", 711 " { if (a_cycles)", 712 " { /* moves through these states are visible */", 713 " #if PROG_LAB>0 && defined(HAS_NP)", 714 " if (progstate[n][i])", 715 " goto degrade;", 716 " for (T1 = trans[n][i]; T1; T1 = T1->nxt)", 717 " if (progstate[n][T1->st])", 718 " goto degrade;", 719 " #endif", 720 " if (accpstate[n][i] || visstate[n][i])", 721 " goto degrade;", 722 " for (T1 = trans[n][i]; T1; T1 = T1->nxt)", 723 " if (accpstate[n][T1->st])", 724 " goto degrade;", 725 " }", 726 " T1 = trans[n][i];", 727 " if (!T1) continue;", 728 " g = mark_safety(T1); /* V3.3.1 */", 729 " if (g < 0) goto degrade; /* global */", 730 " /* check if mixing of guards preserves reduction */", 731 " if (T1->nxt)", 732 " { k = 0;", 733 " for (T0 = T1; T0; T0 = T0->nxt)", 734 " { if (!(T0->atom&8))", 735 " goto degrade;", 736 " for (aa = 0; aa < 2; aa++)", 737 " { j = srinc_set(T0->tpe[aa]);", 738 " if (j >= GLOBAL && j != ALPHA_F)", 739 " goto degrade;", 740 " if (T0->tpe[aa]", 741 " && T0->tpe[aa]", 742 " != T1->tpe[0])", 743 " k = 1;", 744 " } }", 745 " /* g = 0; V3.3.1 */", 746 " if (k) /* non-uniform selection */", 747 " for (T0 = T1; T0; T0 = T0->nxt)", 748 " for (aa = 0; aa < 2; aa++)", 749 " { j = srinc_set(T0->tpe[aa]);", 750 " if (j != LOCAL)", 751 " { k = srunc(T0->tpe[aa], j);", 752 " for (h = 0; h < 6; h++)", 753 " if (T1->qu[h] == k", 754 " && T1->ty[h] == j)", 755 " break;", 756 " if (h >= 6)", 757 " { T1->qu[g%%6] = k;", 758 " T1->ty[g%%6] = j;", 759 " g++;", 760 " } } }", 761 " if (g > 6)", 762 " { T1->qu[0] = 0; /* turn it off */", 763 " printf(\"pan: warning, line %%d, \",", 764 " srcln[i]);", 765 " printf(\"too many stmnt types (%%d)\",", 766 " g);", 767 " printf(\" in selection\\n\");", 768 " goto degrade;", 769 " }", 770 " }", 771 " /* mark all options global if >=1 is global */", 772 " for (T1 = trans[n][i]; T1; T1 = T1->nxt)", 773 " if (!(T1->atom&8)) break;", 774 " if (T1)", 775 "degrade: for (T1 = trans[n][i]; T1; T1 = T1->nxt)", 776 " T1->atom &= ~8; /* mark as unsafe */", 777 778 " /* can only mix 'r's or 's's if on same chan */", 779 " /* and not mixed with other local operations */", 780 " T1 = trans[n][i];", 781 782 " if (!T1 || T1->qu[0]) continue;", 783 784 " j = T1->tpe[0];", 785 " if (T1->nxt && T1->atom&8)", 786 " { if (j == 5*DELTA)", 787 " { printf(\"warning: line %%d \", srcln[i]);", 788 " printf(\"mixed condition \");", 789 " printf(\"(defeats reduction)\\n\");", 790 " goto degrade;", 791 " }", 792 " for (T0 = T1; T0; T0 = T0->nxt)", 793 " for (aa = 0; aa < 2; aa++)", 794 " if (T0->tpe[aa] && T0->tpe[aa] != j)", 795 " { printf(\"warning: line %%d \", srcln[i]);", 796 " printf(\"[%%d-%%d] mixed %%stion \",", 797 " T0->tpe[aa], j, ", 798 " (j==5*DELTA)?\"condi\":\"selec\");", 799 " printf(\"(defeats reduction)\\n\");", 800 " printf(\" '%%s' <-> '%%s'\\n\",", 801 " T1->tp, T0->tp);", 802 " goto degrade;", 803 " } }", 804 " }", 805 "#endif", 806 " for (i = 1; i < m; i++)", /* R */ 807 " { T2 = trans[n][i];", 808 " if (!T2", 809 " || T2->nxt", 810 " || strncmp(T2->tp, \".(goto)\", 7)", 811 " || !stopstate[n][i])", 812 " continue;", 813 " stopstate[n][T2->st] = 1;", 814 " }", 815 " if (state_tables && !verbose)", 816 " { if (dodot)", 817 " { char buf[256], *q = buf, *p = procname[n];", 818 " while (*p != '\\0')", 819 " { if (*p != ':')", 820 " { *q++ = *p;", 821 " }", 822 " p++;", 823 " }", 824 " *q = '\\0';", 825 " printf(\"digraph \");", 826 " switch (Btypes[n]) {", 827 " case I_PROC: printf(\"init {\\n\"); break;", 828 " case N_CLAIM: printf(\"claim_%%s {\\n\", buf); break;", 829 " case E_TRACE: printf(\"notrace {\\n\"); break;", 830 " case N_TRACE: printf(\"trace {\\n\"); break;", 831 " default: printf(\"p_%%s {\\n\", buf); break;", 832 " }", 833 " printf(\"size=\\\"8,10\\\";\\n\");", 834 " printf(\" GT [shape=box,style=dotted,label=\\\"%%s\\\"];\\n\", buf);", 835 " } else", 836 " { switch (Btypes[n]) {", 837 " case I_PROC: printf(\"init\\n\"); break;", 838 " case N_CLAIM: printf(\"claim %%s\\n\", procname[n]); break;", 839 " case E_TRACE: printf(\"notrace assertion\\n\"); break;", 840 " case N_TRACE: printf(\"trace assertion\\n\"); break;", 841 " default: printf(\"proctype %%s\\n\", procname[n]); break;", 842 " } }", 843 " for (i = 1; i < m; i++)", 844 " { reach[i] = 1;", 845 " }", 846 " tagtable(n, m, is, srcln, reach);", 847 " if (dodot) printf(\"}\\n\");", 848 " } else", 849 " for (i = 1; i < m; i++)", 850 " { int nrelse;", 851 " if (Btypes[n] != N_CLAIM)", 852 " { for (T0 = trans[n][i]; T0; T0 = T0->nxt)", 853 " { if (T0->st == i", 854 " && strcmp(T0->tp, \"(1)\") == 0)", 855 " { printf(\"error: proctype '%%s' \",", 856 " procname[n]);", 857 " printf(\"line %%d, state %%d: has un\",", 858 " srcln[i], i);", 859 " printf(\"conditional self-loop\\n\");", 860 " pan_exit(1);", 861 " } } }", 862 " nrelse = 0;", 863 " for (T0 = trans[n][i]; T0; T0 = T0->nxt)", 864 " { if (strcmp(T0->tp, \"else\") == 0)", 865 " nrelse++;", 866 " }", 867 " if (nrelse > 1)", 868 " { printf(\"error: proctype '%%s' state\",", 869 " procname[n]);", 870 " printf(\" %%d, inherits %%d\", i, nrelse);", 871 " printf(\" 'else' stmnts\\n\");", 872 " pan_exit(1);", 873 " } }", 874 "#ifndef LOOPSTATE", 875 " if (state_tables)", 876 "#endif", 877 " do_dfs(n, m, is, srcln, reach, lstate);", 878 "#ifdef T_REVERSE", 879 " /* process n, with m states, is=initial state -- reverse list */", 880 " if (!state_tables && Btypes[n] != N_CLAIM)", 881 " { for (i = 1; i < m; i++)", /* for each state */ 882 " { Trans *Tx = (Trans *) 0; /* list of escapes */", 883 " Trans *Ty = (Trans *) 0; /* its tail element */", 884 " T1 = (Trans *) 0; /* reversed list */", 885 " T2 = (Trans *) 0; /* its tail */", 886 " T3 = (Trans *) 0; /* remembers possible 'else' */", 887 "", 888 " /* find unless-escapes, they should go first */", 889 " T4 = T5 = T0 = trans[n][i];", 890 "#ifdef HAS_UNLESS", 891 " while (T4 && T4->e_trans) /* escapes are first in orig list */", 892 " { T5 = T4; /* remember predecessor */", 893 " T4 = T4->nxt;", 894 " }", 895 "#endif", 896 " /* T4 points to first non-escape, T5 to its parent, T0 to original list */", 897 " if (T4 != T0) /* there was at least one escape */", 898 " { T3 = T5->nxt; /* start of non-escapes */", 899 " T5->nxt = (Trans *) 0; /* separate */", 900 " Tx = T0; /* start of the escapes */", 901 " Ty = T5; /* its tail */", 902 " T0 = T3; /* the rest, to be reversed */", 903 " }", 904 " /* T0 points to first non-escape, Tx to the list of escapes, Ty to its tail */", 905 "", 906 " /* first tail-add non-escape transitions, reversed */", 907 " T3 = (Trans *) 0;", /* remember a possible 'else' */ 908 " for (T5 = T0; T5; T5 = T4)", 909 " { T4 = T5->nxt;", 910 "#ifdef HAS_UNLESS", 911 " if (T5->e_trans)", 912 " { printf(\"error: cannot happen!\\n\");", 913 " continue;", 914 " }", 915 "#endif", 916 " if (strcmp(T5->tp, \"else\") == 0)", 917 " { T3 = T5;", 918 " T5->nxt = (Trans *) 0;", 919 " } else", 920 " { T5->nxt = T1;", 921 " if (!T1) { T2 = T5; }", 922 " T1 = T5;", 923 " } }", 924 " /* T3 points to a possible else, which is removed from the list */", 925 " /* T1 points to the reversed list so far (without escapes) */", 926 " /* T2 points to the tail element -- where the else should go */", 927 " if (T2 && T3) { T2->nxt = T3; } /* add else */", 928 "", 929 " /* add in the escapes, to that they appear at the front */", 930 " if (Tx && Ty) { Ty->nxt = T1; T1 = Tx; }", 931 "", 932 " trans[n][i] = T1;", 933 " /* reversed, with escapes first and else last */", 934 " } }", 935 " if (state_tables && verbose)", 936 " { printf(\"FINAL proctype %%s\\n\", ", 937 " procname[n]);", 938 " for (i = 1; i < m; i++)", 939 " for (T0 = trans[n][i]; T0; T0 = T0->nxt)", 940 " crack(n, i, T0, srcln);", 941 " }", 942 "#endif", 943 "}", 944 "void", 945 "imed(Trans *T, int v, int n, int j) /* set intermediate state */", 946 "{ progstate[n][T->st] |= progstate[n][v];", 947 " accpstate[n][T->st] |= accpstate[n][v];", 948 " stopstate[n][T->st] |= stopstate[n][v];", 949 " mapstate[n][j] = T->st;", 950 "}", 951 "void", 952 "tagtable(int n, int m, int is, short srcln[], uchar reach[])", 953 "{ Trans *z;\n", 954 " if (is >= m || !trans[n][is]", 955 " || is <= 0 || reach[is] == 0)", 956 " return;", 957 " reach[is] = 0;", 958 " if (state_tables)", 959 " for (z = trans[n][is]; z; z = z->nxt)", 960 " { if (dodot)", 961 " dot_crack(n, is, z);", 962 " else", 963 " crack(n, is, z, srcln);", 964 " }", 965 "", 966 " for (z = trans[n][is]; z; z = z->nxt)", 967 " {", 968 "#ifdef HAS_UNLESS", 969 " int i, j;", 970 "#endif", 971 " tagtable(n, m, z->st, srcln, reach);", 972 "#ifdef HAS_UNLESS", 973 " for (i = 0; i < HAS_UNLESS; i++)", 974 " { j = trans[n][is]->escp[i];", 975 " if (!j) break;", 976 " tagtable(n, m, j, srcln, reach);", 977 " }", 978 "#endif", 979 " }", 980 "}", 981 "void", 982 "dfs_table(int n, int m, int is, short srcln[], uchar reach[], uchar lstate[])", 983 "{ Trans *z;\n", 984 " if (is >= m || is <= 0 || !trans[n][is])", 985 " return;", 986 " if ((reach[is] & (4|8|16)) != 0)", 987 " { if ((reach[is] & (8|16)) == 16) /* on stack, not yet recorded */", 988 " { lstate[is] = 1;", 989 " reach[is] |= 8; /* recorded */", 990 " if (state_tables && verbose)", 991 " { printf(\"state %%d line %%d is a loopstate\\n\", is, srcln[is]);", 992 " } }", 993 " return;", 994 " }", 995 " reach[is] |= (4|16); /* visited | onstack */", 996 " for (z = trans[n][is]; z; z = z->nxt)", 997 " {", 998 "#ifdef HAS_UNLESS", 999 " int i, j;", 1000 "#endif", 1001 " dfs_table(n, m, z->st, srcln, reach, lstate);", 1002 "#ifdef HAS_UNLESS", 1003 " for (i = 0; i < HAS_UNLESS; i++)", 1004 " { j = trans[n][is]->escp[i];", 1005 " if (!j) break;", 1006 " dfs_table(n, m, j, srcln, reach, lstate);", 1007 " }", 1008 "#endif", 1009 " }", 1010 " reach[is] &= ~16; /* no longer on stack */", 1011 "}", 1012 "void", 1013 "do_dfs(int n, int m, int is, short srcln[], uchar reach[], uchar lstate[])", 1014 "{ int i;", 1015 " dfs_table(n, m, is, srcln, reach, lstate);", 1016 " for (i = 0; i < m; i++)", 1017 " reach[i] &= ~(4|8|16);", 1018 "}", 1019 "void", 1020 "crack(int n, int j, Trans *z, short srcln[])", 1021 "{ int i;\n", 1022 " if (!z) return;", 1023 " printf(\"\tstate %%3d -(tr %%3d)-> state %%3d \",", 1024 " j, z->forw, z->st);", 1025 " printf(\"[id %%3d tp %%3d\", z->t_id, z->tpe[0]);", 1026 " if (z->tpe[1]) printf(\",%%d\", z->tpe[1]);", 1027 "#ifdef HAS_UNLESS", 1028 " if (z->e_trans)", 1029 " printf(\" org %%3d\", z->e_trans);", 1030 " else if (state_tables >= 2)", 1031 " for (i = 0; i < HAS_UNLESS; i++)", 1032 " { if (!z->escp[i]) break;", 1033 " printf(\" esc %%d\", z->escp[i]);", 1034 " }", 1035 "#endif", 1036 " printf(\"]\");", 1037 " printf(\" [%%s%%s%%s%%s%%s] %%s:%%d => \",", 1038 " z->atom&6?\"A\":z->atom&32?\"D\":\"-\",", 1039 " accpstate[n][j]?\"a\" :\"-\",", 1040 " stopstate[n][j]?\"e\" : \"-\",", 1041 " progstate[n][j]?\"p\" : \"-\",", 1042 " z->atom & 8 ?\"L\":\"G\",", 1043 " PanSource, srcln[j]);", 1044 " for (i = 0; z->tp[i]; i++)", 1045 " if (z->tp[i] == \'\\n\')", 1046 " printf(\"\\\\n\");", 1047 " else", 1048 " putchar(z->tp[i]);", 1049 " if (verbose && z->qu[0])", 1050 " { printf(\"\\t[\");", 1051 " for (i = 0; i < 6; i++)", 1052 " if (z->qu[i])", 1053 " printf(\"(%%d,%%d)\",", 1054 " z->qu[i], z->ty[i]);", 1055 " printf(\"]\");", 1056 " }", 1057 " printf(\"\\n\");", 1058 " fflush(stdout);", 1059 "}", 1060 "/* spin -a m.pml; cc -o pan pan.c; ./pan -D | dot -Tps > foo.ps; ps2pdf foo.ps */", 1061 "void", 1062 "dot_crack(int n, int j, Trans *z)", 1063 "{ int i;\n", 1064 " if (!z) return;", 1065 " printf(\"\tS%%d -> S%%d [color=black\", j, z->st);", 1066 "", 1067 " if (z->atom&6) printf(\",style=dashed\");", /* A */ 1068 " else if (z->atom&32) printf(\",style=dotted\");", /* D */ 1069 " else if (z->atom&8) printf(\",style=solid\");", /* L */ 1070 " else printf(\",style=bold\");", /* G */ 1071 /* other styles: filled dotted */ 1072 "", 1073 " printf(\",label=\\\"\");", 1074 " for (i = 0; z->tp[i]; i++)", 1075 " { if (z->tp[i] == \'\\\\\'", 1076 " && z->tp[i+1] == \'n\')", 1077 " { i++; printf(\" \");", 1078 " } else", 1079 " { putchar(z->tp[i]);", 1080 " } }", 1081 " printf(\"\\\"];\\n\");", 1082 " if (accpstate[n][j]) printf(\" S%%d [color=red,style=bold];\\n\", j);", 1083 " else if (progstate[n][j]) printf(\" S%%d [color=green,style=bold];\\n\", j);", 1084 " if (stopstate[n][j]) printf(\" S%%d [color=blue,style=bold,shape=box];\\n\", j);", 1085 "}", 1086 "", 1087 "#ifdef VAR_RANGES", 1088 "#define BYTESIZE 32 /* 2^8 : 2^3 = 256:8 = 32 */", 1089 "", 1090 "typedef struct Vr_Ptr {", 1091 " char *nm;", 1092 " uchar vals[BYTESIZE];", 1093 " struct Vr_Ptr *nxt;", 1094 "} Vr_Ptr;", 1095 "Vr_Ptr *ranges = (Vr_Ptr *) 0;", 1096 "", 1097 "void", 1098 "logval(char *s, int v)", 1099 "{ Vr_Ptr *tmp;", 1100 "", 1101 " if (v<0 || v > 255) return;", 1102 " for (tmp = ranges; tmp; tmp = tmp->nxt)", 1103 " if (!strcmp(tmp->nm, s))", 1104 " goto found;", 1105 " tmp = (Vr_Ptr *) emalloc(sizeof(Vr_Ptr));", 1106 " tmp->nxt = ranges;", 1107 " ranges = tmp;", 1108 " tmp->nm = s;", 1109 "found:", 1110 " tmp->vals[(v)/8] |= 1<<((v)%%8);", 1111 "}", 1112 "", 1113 "void", 1114 "dumpval(uchar X[], int range)", 1115 "{ int w, x, i, j = -1;", 1116 "", 1117 " for (w = i = 0; w < range; w++)", 1118 " for (x = 0; x < 8; x++, i++)", 1119 " {", 1120 "from: if ((X[w] & (1<<x)))", 1121 " { printf(\"%%d\", i);", 1122 " j = i;", 1123 " goto upto;", 1124 " } }", 1125 " return;", 1126 " for (w = 0; w < range; w++)", 1127 " for (x = 0; x < 8; x++, i++)", 1128 " {", 1129 "upto: if (!(X[w] & (1<<x)))", 1130 " { if (i-1 == j)", 1131 " printf(\", \");", 1132 " else", 1133 " printf(\"-%%d, \", i-1);", 1134 " goto from;", 1135 " } }", 1136 " if (j >= 0 && j != 255)", 1137 " printf(\"-255\");", 1138 "}", 1139 "", 1140 "void", 1141 "dumpranges(void)", 1142 "{ Vr_Ptr *tmp;", 1143 " printf(\"\\nValues assigned within \");", 1144 " printf(\"interval [0..255]:\\n\");", 1145 " for (tmp = ranges; tmp; tmp = tmp->nxt)", 1146 " { printf(\"\\t%%s\\t: \", tmp->nm);", 1147 " dumpval(tmp->vals, BYTESIZE);", 1148 " printf(\"\\n\");", 1149 " }", 1150 "}", 1151 "#endif", 1152 0, 1153 }; 1154