1: #include <flx_categories.flxh> 2: 3: include "std"; 4: header std_stl_vector = "#include <vector>"; 5: header std_stl_list = "#include <list>"; 6: header std_stl_deque = "#include <deque>"; 7: header std_stl_queue = "#include <queue>"; 8: header std_stl_set = "#include <set>"; 9: header std_stl_map = "#include <map>"; 10: header std_stl_stack = "#include <stack>"; 11: header ext_hash_set = "#include <ext/hash_set>"; 12: header ext_hash_map = "#include <ext/hash_map>"; 13: header ext_slist = "#include <ext/slist>"; 14: // hash for std::string for use with hash containers 15: header ext_string_hash = """ 16: namespace __gnu_cxx { 17: template<> struct hash<std::string> { 18: size_t operator()(std::string const& s)const; 19: }; 20: } 21: """; 22: 23: body ext_string_hash = """ 24: // this is a sick hash .. fix it! 25: size_t __gnu_cxx::hash<std::string>:: 26: operator()(std::string const& s)const { 27: char const *p = s.data(); 28: int n = s.size(); 29: int h = 0; 30: for(; n; --n,++p) h+= 5 * *p; 31: return h; 32: } 33: """; 34: 35: module Stl 36: { 37: type pair[k,v] = "std::pair<?1 const,?2>"; 38: fun make_pair[k,v]: k * v ->pair[k,v] = "std::make_pair($1,$2)"; 39: 40: module Vector[t] 41: { 42: requires std_stl_vector; 43: type stl_vector = "std::vector<?1>"; 44: fun create : unit -> stl_vector[t] = "(GXX_PARSER_HACK std::vector<?1>())"; 45: fun create : int * t -> stl_vector[t]= "(GXX_PARSER_HACK std::vector<?1>($1,$2))"; 46: fun create[i] : i * i -> stl_vector[t] = "(GXX_PARSER_HACK std::vector<?1>($1,$2))"; 47: gen_cmp stl_vector[t]; 48: fun len: stl_vector[t] -> int = "$1.size()"; 49: fun empty: stl_vector[t] -> int = "$1.empty()"; 50: type stl_vector_iterator = "std::vector<?1>::iterator"; 51: gen_cmp stl_vector_iterator[t]; 52: gen_forward stl_vector_iterator[t]; 53: fun deref : stl_vector_iterator[t] -> lvalue[t] = "*$1"; 54: fun begin : stl_vector[t]-> stl_vector_iterator[t]= "$1.begin()"; 55: fun end : stl_vector[t]-> stl_vector_iterator[t]= "$1.end()"; 56: proc erase : stl_vector[t] * stl_vector_iterator[t] = "$1.erase($1);"; 57: proc erase : stl_vector[t] * stl_vector_iterator[t] * stl_vector_iterator[t] = "$1.erase($1,$2);"; 58: proc clear : stl_vector[t] = "$1.clear();"; 59: proc pre_incr : lvalue[stl_vector_iterator[t]] = "++$1;"; 60: proc post_incr : stl_vector_iterator[t] = "++$1;"; 61: proc pre_decr : lvalue[stl_vector_iterator[t]] = "--$1;"; 62: proc post_decr : stl_vector_iterator[t] = "--$1;"; 63: type stl_vector_reverse_iterator = "std::vector<?1>::reverse_iterator"; 64: fun rbegin : stl_vector[t]-> stl_vector_reverse_iterator[t]= "$1.rbegin()"; 65: fun rend : stl_vector[t]-> stl_vector_reverse_iterator[t]= "$1.rend()"; 66: fun deref : stl_vector_reverse_iterator[t] -> lvalue[t] = "*$1"; 67: gen_cmp stl_vector_reverse_iterator[t]; 68: proc pre_incr : lvalue[stl_vector_reverse_iterator[t]] = "++$1;"; 69: proc post_incr : stl_vector_reverse_iterator[t] = "++$1;"; 70: proc pre_decr: lvalue[stl_vector_reverse_iterator[t]] = "--$1;"; 71: proc post_decr : stl_vector_reverse_iterator[t] = "--$1;"; 72: proc insert: stl_vector[t] * stl_vector_iterator[t] * t = "$1.insert($2,$3);"; 73: proc push_back : stl_vector[t] * t = "$1.push_back($2);"; 74: fun front : stl_vector[t] -> t = "$1.front()"; 75: fun front : stl_vector[t] -> t = "$1.front()"; 76: fun subscript : lvalue[stl_vector[t]] * int -> lvalue[t] = "$1.at($2)"; 77: fun subscript : stl_vector[t] * int -> t = "$1.at($2)"; 78: fun add: stl_vector_iterator[t] * int -> stl_vector_iterator[t] = "$1+$2"; 79: fun sub: stl_vector_iterator[t] * int -> stl_vector_iterator[t] = "$1-$2"; 80: proc pluseq: lvalue[stl_vector_iterator[t]] * int = "$1+=$2;"; 81: proc minuseq: lvalue[stl_vector_iterator[t]] * int -> stl_vector_iterator[t] = "$1-=$2;"; 82: fun subscript: stl_vector_iterator[t] * int -> lvalue[t] = "$1[$2]"; 83: } 84: module List[t] 85: { 86: requires std_stl_list; 87: type stl_list = "std::list<?1>"; 88: fun create : unit -> stl_list[t] = "(GXX_PARSER_HACK std::list<?1>())"; 89: fun create : int * t -> stl_list[t]= "(GXX_PARSER_HACK std::list<?1>($1,$2))"; 90: fun create[i] : i * i -> stl_list[t] = "(GXX_PARSER_HACK std::list<?1>($1,$2))"; 91: gen_cmp stl_list[t]; 92: fun len: stl_list[t] -> int = "$1.size()"; 93: fun empty: stl_list[t] -> int = "$1.empty()"; 94: type stl_list_iterator = "std::list<?1>::iterator"; 95: gen_cmp stl_list_iterator[t]; 96: gen_forward stl_list_iterator[t]; 97: fun deref : stl_list_iterator[t] -> lvalue[t] = "*$1"; 98: fun begin : stl_list[t]-> stl_list_iterator[t]= "$1.begin()"; 99: fun end : stl_list[t]-> stl_list_iterator[t]= "$1.end()"; 100: proc erase : stl_list[t] * stl_list_iterator[t] = "$1.erase($1);"; 101: proc erase : stl_list[t] * stl_list_iterator[t] * stl_list_iterator[t] = "$1.erase($1,$2);"; 102: proc clear : stl_list[t] = "$1.clear();"; 103: proc pre_incr : lvalue[stl_list_iterator[t]] = "++$1;"; 104: proc post_incr : stl_list_iterator[t] = "++$1;"; 105: proc pre_decr : lvalue[stl_list_iterator[t]] = "--$1;"; 106: proc post_decr : stl_list_iterator[t] = "--$1;"; 107: type stl_list_reverse_iterator = "std::list<?1>::reverse_iterator"; 108: fun rbegin : stl_list[t]-> stl_list_reverse_iterator[t]= "$1.rbegin()"; 109: fun rend : stl_list[t]-> stl_list_reverse_iterator[t]= "$1.rend()"; 110: fun deref : stl_list_reverse_iterator[t] -> lvalue[t] = "*$1"; 111: gen_cmp stl_list_reverse_iterator[t]; 112: proc pre_incr : lvalue[stl_list_reverse_iterator[t]] = "++$1;"; 113: proc post_incr : stl_list_reverse_iterator[t] = "++$1;"; 114: proc pre_decr: lvalue[stl_list_reverse_iterator[t]] = "--$1;"; 115: proc post_decr : stl_list_reverse_iterator[t] = "--$1;"; 116: proc insert: stl_list[t] * stl_list_iterator[t] * t = "$1.insert($2,$3);"; 117: proc push_front : stl_list[t] * t = "$1.push_front($2);"; 118: proc push_back : stl_list[t] * t = "$1.push_back($2);"; 119: fun front : stl_list[t] -> t = "$1.front()"; 120: fun front : stl_list[t] -> t = "$1.front()"; 121: proc pop_front : stl_list[t] = "$1.pop_back();"; 122: } 123: module Queue[t] 124: { 125: requires std_stl_queue; 126: type stl_queue = "std::queue<?1>"; 127: fun create : unit -> stl_queue[t] = "(GXX_PARSER_HACK std::queue<?1>())"; 128: fun create : int * t -> stl_queue[t]= "(GXX_PARSER_HACK std::queue<?1>($1,$2))"; 129: fun create[i] : i * i -> stl_queue[t] = "(GXX_PARSER_HACK std::queue<?1>($1,$2))"; 130: gen_cmp stl_queue[t]; 131: fun len: stl_queue[t] -> int = "$1.size()"; 132: fun empty: stl_queue[t] -> int = "$1.empty()"; 133: type stl_queue_iterator = "std::queue<?1>::iterator"; 134: gen_cmp stl_queue_iterator[t]; 135: gen_forward stl_queue_iterator[t]; 136: fun deref : stl_queue_iterator[t] -> lvalue[t] = "*$1"; 137: fun begin : stl_queue[t]-> stl_queue_iterator[t]= "$1.begin()"; 138: fun end : stl_queue[t]-> stl_queue_iterator[t]= "$1.end()"; 139: proc erase : stl_queue[t] * stl_queue_iterator[t] = "$1.erase($1);"; 140: proc erase : stl_queue[t] * stl_queue_iterator[t] * stl_queue_iterator[t] = "$1.erase($1,$2);"; 141: proc clear : stl_queue[t] = "$1.clear();"; 142: proc pre_incr : lvalue[stl_queue_iterator[t]] = "++$1;"; 143: proc post_incr : stl_queue_iterator[t] = "++$1;"; 144: proc pre_decr : lvalue[stl_queue_iterator[t]] = "--$1;"; 145: proc post_decr : stl_queue_iterator[t] = "--$1;"; 146: proc insert: stl_queue[t] * stl_queue_iterator[t] * t = "$1.insert($2,$3);"; 147: } 148: module Deque[t] 149: { 150: requires std_stl_deque; 151: type stl_deque = "std::deque<?1>"; 152: fun create : unit -> stl_deque[t] = "(GXX_PARSER_HACK std::deque<?1>())"; 153: fun create : int * t -> stl_deque[t]= "(GXX_PARSER_HACK std::deque<?1>($1,$2))"; 154: fun create[i] : i * i -> stl_deque[t] = "(GXX_PARSER_HACK std::deque<?1>($1,$2))"; 155: gen_cmp stl_deque[t]; 156: fun len: stl_deque[t] -> int = "$1.size()"; 157: fun empty: stl_deque[t] -> int = "$1.empty()"; 158: type stl_deque_iterator = "std::deque<?1>::iterator"; 159: gen_cmp stl_deque_iterator[t]; 160: gen_forward stl_deque_iterator[t]; 161: fun deref : stl_deque_iterator[t] -> lvalue[t] = "*$1"; 162: fun begin : stl_deque[t]-> stl_deque_iterator[t]= "$1.begin()"; 163: fun end : stl_deque[t]-> stl_deque_iterator[t]= "$1.end()"; 164: proc erase : stl_deque[t] * stl_deque_iterator[t] = "$1.erase($1);"; 165: proc erase : stl_deque[t] * stl_deque_iterator[t] * stl_deque_iterator[t] = "$1.erase($1,$2);"; 166: proc clear : stl_deque[t] = "$1.clear();"; 167: proc pre_incr : lvalue[stl_deque_iterator[t]] = "++$1;"; 168: proc post_incr : stl_deque_iterator[t] = "++$1;"; 169: proc pre_decr : lvalue[stl_deque_iterator[t]] = "--$1;"; 170: proc post_decr : stl_deque_iterator[t] = "--$1;"; 171: type stl_deque_reverse_iterator = "std::deque<?1>::reverse_iterator"; 172: fun rbegin : stl_deque[t]-> stl_deque_reverse_iterator[t]= "$1.rbegin()"; 173: fun rend : stl_deque[t]-> stl_deque_reverse_iterator[t]= "$1.rend()"; 174: fun deref : stl_deque_reverse_iterator[t] -> lvalue[t] = "*$1"; 175: gen_cmp stl_deque_reverse_iterator[t]; 176: proc pre_incr : lvalue[stl_deque_reverse_iterator[t]] = "++$1;"; 177: proc post_incr : stl_deque_reverse_iterator[t] = "++$1;"; 178: proc pre_decr: lvalue[stl_deque_reverse_iterator[t]] = "--$1;"; 179: proc post_decr : stl_deque_reverse_iterator[t] = "--$1;"; 180: proc insert: stl_deque[t] * stl_deque_iterator[t] * t = "$1.insert($2,$3);"; 181: proc push_front : stl_deque[t] * t = "$1.push_front($2);"; 182: proc push_back : stl_deque[t] * t = "$1.push_back($2);"; 183: proc pop_front : stl_deque[t] = "$1.pop_back();"; 184: fun front : stl_deque[t] -> t = "$1.front()"; 185: fun front : stl_deque[t] -> t = "$1.front()"; 186: fun subscript : lvalue[stl_deque[t]] * int -> lvalue[t] = "$1.at($2)"; 187: fun subscript : stl_deque[t] * int -> t = "$1.at($2)"; 188: } 189: module PriorityQueue[t] 190: { 191: requires std_stl_queue; 192: type stl_priorityqueue = "std::priorityqueue<?1>"; 193: fun create : unit -> stl_priorityqueue[t] = "(GXX_PARSER_HACK std::priorityqueue<?1>())"; 194: fun create : int * t -> stl_priorityqueue[t]= "(GXX_PARSER_HACK std::priorityqueue<?1>($1,$2))"; 195: fun create[i] : i * i -> stl_priorityqueue[t] = "(GXX_PARSER_HACK std::priorityqueue<?1>($1,$2))"; 196: gen_cmp stl_priorityqueue[t]; 197: fun len: stl_priorityqueue[t] -> int = "$1.size()"; 198: fun empty: stl_priorityqueue[t] -> int = "$1.empty()"; 199: type stl_priorityqueue_iterator = "std::priorityqueue<?1>::iterator"; 200: gen_cmp stl_priorityqueue_iterator[t]; 201: gen_forward stl_priorityqueue_iterator[t]; 202: fun deref : stl_priorityqueue_iterator[t] -> lvalue[t] = "*$1"; 203: fun begin : stl_priorityqueue[t]-> stl_priorityqueue_iterator[t]= "$1.begin()"; 204: fun end : stl_priorityqueue[t]-> stl_priorityqueue_iterator[t]= "$1.end()"; 205: proc erase : stl_priorityqueue[t] * stl_priorityqueue_iterator[t] = "$1.erase($1);"; 206: proc erase : stl_priorityqueue[t] * stl_priorityqueue_iterator[t] * stl_priorityqueue_iterator[t] = "$1.erase($1,$2);"; 207: proc clear : stl_priorityqueue[t] = "$1.clear();"; 208: proc pre_incr : lvalue[stl_priorityqueue_iterator[t]] = "++$1;"; 209: proc post_incr : stl_priorityqueue_iterator[t] = "++$1;"; 210: proc pre_decr : lvalue[stl_priorityqueue_iterator[t]] = "--$1;"; 211: proc post_decr : stl_priorityqueue_iterator[t] = "--$1;"; 212: } 213: module Stack[t] 214: { 215: requires std_stl_stack; 216: type stl_stack = "std::stack<?1>"; 217: fun create : unit -> stl_stack[t] = "(GXX_PARSER_HACK std::stack<?1>())"; 218: fun create : int * t -> stl_stack[t]= "(GXX_PARSER_HACK std::stack<?1>($1,$2))"; 219: fun create[i] : i * i -> stl_stack[t] = "(GXX_PARSER_HACK std::stack<?1>($1,$2))"; 220: gen_cmp stl_stack[t]; 221: fun len: stl_stack[t] -> int = "$1.size()"; 222: fun empty: stl_stack[t] -> int = "$1.empty()"; 223: type stl_stack_iterator = "std::stack<?1>::iterator"; 224: gen_cmp stl_stack_iterator[t]; 225: gen_forward stl_stack_iterator[t]; 226: fun deref : stl_stack_iterator[t] -> lvalue[t] = "*$1"; 227: fun begin : stl_stack[t]-> stl_stack_iterator[t]= "$1.begin()"; 228: fun end : stl_stack[t]-> stl_stack_iterator[t]= "$1.end()"; 229: proc erase : stl_stack[t] * stl_stack_iterator[t] = "$1.erase($1);"; 230: proc erase : stl_stack[t] * stl_stack_iterator[t] * stl_stack_iterator[t] = "$1.erase($1,$2);"; 231: proc clear : stl_stack[t] = "$1.clear();"; 232: proc pre_incr : lvalue[stl_stack_iterator[t]] = "++$1;"; 233: proc post_incr : stl_stack_iterator[t] = "++$1;"; 234: proc pre_decr : lvalue[stl_stack_iterator[t]] = "--$1;"; 235: proc post_decr : stl_stack_iterator[t] = "--$1;"; 236: } 237: 238: module Set[t] 239: { 240: requires std_stl_set; 241: type stl_set = "std::set<?1>"; 242: type stl_set_iterator = "std::set<?1>::iterator"; 243: type stl_set_reverse_iterator = "std::set<?1>::reverse_iterator"; 244: fun create : unit -> stl_set[t] = "(GXX_PARSER_HACK std::set<?1>())"; 245: gen_cmp stl_set[t]; 246: fun len: stl_set[t]->int = "$1.size()"; 247: fun empty: stl_set[t]->int = "$1.empty()"; 248: gen_cmp stl_set_iterator[t]; 249: gen_cmp stl_set_reverse_iterator[t]; 250: proc pre_incr : lvalue[stl_set_iterator[t]] = "++$1;"; 251: proc post_incr : stl_set_iterator[t] = "++$1;"; 252: proc pre_incr : lvalue[stl_set_reverse_iterator[t]] = "++$1;"; 253: proc post_incr : stl_set_reverse_iterator[t] = "++$1;"; 254: proc pre_decr : lvalue[stl_set_iterator[t]] = "--$1;"; 255: proc post_decr : stl_set_iterator[t] = "--$1;"; 256: proc pre_decr: lvalue[stl_set_reverse_iterator[t]] = "--$1;"; 257: proc post_decr : stl_set_reverse_iterator[t] = "--$1;"; 258: fun deref : stl_set_iterator[t] -> t = "*(#0*)&*$1:unary" is unary; 259: fun deref : stl_set_reverse_iterator[t] -> t = "*(#0*)&*$1:unary" is unary; 260: fun begin : stl_set[t]-> stl_set_iterator[t]= "$1.begin()"; 261: fun end : stl_set[t]-> stl_set_iterator[t]= "$1.end()"; 262: fun rbegin : stl_set[t]-> stl_set_reverse_iterator[t]= "$1.rbegin()"; 263: fun rend : stl_set[t]-> stl_set_reverse_iterator[t]= "$1.rend()"; 264: proc insert : stl_set[t] * t = "$1.insert($2);"; 265: proc erase : stl_set[t] * stl_set_iterator[t] = "$1.erase($1);"; 266: proc clear : stl_set[t] = "$1.clear();"; 267: fun find : stl_set[t] * t -> stl_set_iterator[t] = "$1.find($2)"; 268: fun mem : stl_set[t] * t -> bool = "$1.find($2) != $1.end()"; 269: } 270: module MultiSet[t] 271: { 272: requires std_stl_set; 273: type stl_multiset = "std::multiset<?1>"; 274: type stl_multiset_iterator = "std::multiset<?1>::iterator"; 275: type stl_multiset_reverse_iterator = "std::multiset<?1>::reverse_iterator"; 276: fun create : unit -> stl_multiset[t] = "(GXX_PARSER_HACK std::multiset<?1>())"; 277: gen_cmp stl_multiset[t]; 278: fun len: stl_multiset[t]->int = "$1.size()"; 279: fun empty: stl_multiset[t]->int = "$1.empty()"; 280: gen_cmp stl_multiset_iterator[t]; 281: gen_cmp stl_multiset_reverse_iterator[t]; 282: proc pre_incr : lvalue[stl_multiset_iterator[t]] = "++$1;"; 283: proc post_incr : stl_multiset_iterator[t] = "++$1;"; 284: proc pre_incr : lvalue[stl_multiset_reverse_iterator[t]] = "++$1;"; 285: proc post_incr : stl_multiset_reverse_iterator[t] = "++$1;"; 286: proc pre_decr : lvalue[stl_multiset_iterator[t]] = "--$1;"; 287: proc post_decr : stl_multiset_iterator[t] = "--$1;"; 288: proc pre_decr: lvalue[stl_multiset_reverse_iterator[t]] = "--$1;"; 289: proc post_decr : stl_multiset_reverse_iterator[t] = "--$1;"; 290: fun deref : stl_multiset_iterator[t] -> t = "*(#0*)&*$1:unary" is unary; 291: fun deref : stl_multiset_reverse_iterator[t] -> t = "*(#0*)&*$1:unary" is unary; 292: fun begin : stl_multiset[t]-> stl_multiset_iterator[t]= "$1.begin()"; 293: fun end : stl_multiset[t]-> stl_multiset_iterator[t]= "$1.end()"; 294: fun rbegin : stl_multiset[t]-> stl_multiset_reverse_iterator[t]= "$1.rbegin()"; 295: fun rend : stl_multiset[t]-> stl_multiset_reverse_iterator[t]= "$1.rend()"; 296: proc insert : stl_multiset[t] * t = "$1.insert($2);"; 297: proc erase : stl_multiset[t] * stl_multiset_iterator[t] = "$1.erase($1);"; 298: proc clear : stl_multiset[t] = "$1.clear();"; 299: fun find : stl_multiset[t] * t -> stl_multiset_iterator[t] = "$1.find($2)"; 300: fun mem : stl_multiset[t] * t -> bool = "$1.find($2) != $1.end()"; 301: } 302: module Map[k,v] 303: { 304: requires std_stl_map; 305: type stl_map = "std::map<?1,?2>"; 306: type stl_map_iterator = "std::map<?1,?2>::iterator"; 307: type stl_map_reverse_iterator = "std::map<?1,?2>::reverse_iterator"; 308: fun create : unit -> stl_map[k,v] = "(GXX_PARSER_HACK std::map<?1,?2>())"; 309: gen_cmp stl_map[k,v]; 310: fun len: stl_map[k,v]->int = "$1.size()"; 311: fun empty: stl_map[k,v]->int = "$1.empty()"; 312: gen_cmp stl_map_iterator[k,v]; 313: gen_cmp stl_map_reverse_iterator[k,v]; 314: proc pre_incr : stl_map_iterator[k,v] = "++$1;"; 315: proc post_incr : stl_map_iterator[k,v] = "++$1;"; 316: proc pre_incr : stl_map_reverse_iterator[k,v] = "++$1;"; 317: proc post_incr : stl_map_reverse_iterator[k,v] = "++$1;"; 318: proc pre_decr : stl_map_iterator[k,v] = "--$1;"; 319: proc post_decr : stl_map_iterator[k,v] = "--$1;"; 320: proc pre_decr : stl_map_reverse_iterator[k,v] = "--$1;"; 321: proc post_decr : stl_map_reverse_iterator[k,v] = "--$1;"; 322: fun deref : stl_map_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary; 323: fun begin : stl_map[k,v]-> stl_map_iterator[k,v]= "$1.begin()"; 324: fun end : stl_map[k,v]-> stl_map_iterator[k,v]= "$1.end()"; 325: fun deref : stl_map_reverse_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary; 326: fun rbegin : stl_map[k,v]-> stl_map_reverse_iterator[k,v]= "$1.rbegin()"; 327: fun rend : stl_map[k,v]-> stl_map_reverse_iterator[k,v]= "$1.rend()"; 328: proc insert : stl_map[k,v] * k * v = "$1.insert(std::make_pair($2,$3));"; 329: proc erase : stl_map[k,v] * stl_map_iterator[k,v] = "$1.erase($1);"; 330: proc clear : stl_map[k,v] = "$1.clear();"; 331: fun find : stl_map[k,v] * k -> stl_map_iterator[k,v] = "$1.find($2)"; 332: fun mem : stl_map[k,v] * k -> bool = "$1.find($2) != $1.end()"; 333: fun subscript: stl_map[k,v] * k -> lvalue[v] = "$1[$2]"; 334: } 335: module MultiMap[k,v] 336: { 337: requires std_stl_map; 338: type stl_multimap = "std::multimap<?1,?2>"; 339: type stl_multimap_iterator = "std::multimap<?1,?2>::iterator"; 340: type stl_multimap_reverse_iterator = "std::multimap<?1,?2>::reverse_iterator"; 341: fun create : unit -> stl_multimap[k,v] = "(GXX_PARSER_HACK std::multimap<?1,?2>())"; 342: gen_cmp stl_multimap[k,v]; 343: fun len: stl_multimap[k,v]->int = "$1.size()"; 344: fun empty: stl_multimap[k,v]->int = "$1.empty()"; 345: gen_cmp stl_multimap_iterator[k,v]; 346: gen_cmp stl_multimap_reverse_iterator[k,v]; 347: proc pre_incr : stl_multimap_iterator[k,v] = "++$1;"; 348: proc post_incr : stl_multimap_iterator[k,v] = "++$1;"; 349: proc pre_incr : stl_multimap_reverse_iterator[k,v] = "++$1;"; 350: proc post_incr : stl_multimap_reverse_iterator[k,v] = "++$1;"; 351: proc pre_decr : stl_multimap_iterator[k,v] = "--$1;"; 352: proc post_decr : stl_multimap_iterator[k,v] = "--$1;"; 353: proc pre_decr : stl_multimap_reverse_iterator[k,v] = "--$1;"; 354: proc post_decr : stl_multimap_reverse_iterator[k,v] = "--$1;"; 355: fun deref : stl_multimap_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary; 356: fun begin : stl_multimap[k,v]-> stl_multimap_iterator[k,v]= "$1.begin()"; 357: fun end : stl_multimap[k,v]-> stl_multimap_iterator[k,v]= "$1.end()"; 358: fun deref : stl_multimap_reverse_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary; 359: fun rbegin : stl_multimap[k,v]-> stl_multimap_reverse_iterator[k,v]= "$1.rbegin()"; 360: fun rend : stl_multimap[k,v]-> stl_multimap_reverse_iterator[k,v]= "$1.rend()"; 361: proc insert : stl_multimap[k,v] * k * v = "$1.insert(std::make_pair($2,$3));"; 362: proc erase : stl_multimap[k,v] * stl_multimap_iterator[k,v] = "$1.erase($1);"; 363: proc clear : stl_multimap[k,v] = "$1.clear();"; 364: fun find : stl_multimap[k,v] * k -> stl_multimap_iterator[k,v] = "$1.find($2)"; 365: fun mem : stl_multimap[k,v] * k -> bool = "$1.find($2) != $1.end()"; 366: fun subscript: stl_multimap[k,v] * k -> lvalue[v] = "$1[$2]"; 367: } 368: 369: module Slist[t] 370: { 371: requires ext_slist; 372: type stl_slist = "__gnu_cxx::slist<?1>"; 373: fun create : unit -> stl_slist[t] = "(GXX_PARSER_HACK __gnu_cxx::slist<?1>())"; 374: fun create : int * t -> stl_slist[t]= "(GXX_PARSER_HACK __gnu_cxx::slist<?1>($1,$2))"; 375: fun create[i] : i * i -> stl_slist[t] = "(GXX_PARSER_HACK __gnu_cxx::slist<?1>($1,$2))"; 376: gen_cmp stl_slist[t]; 377: fun len: stl_slist[t] -> int = "$1.size()"; 378: fun empty: stl_slist[t] -> int = "$1.empty()"; 379: type stl_slist_iterator = "__gnu_cxx::slist<?1>::iterator"; 380: gen_cmp stl_slist_iterator[t]; 381: gen_forward stl_slist_iterator[t]; 382: fun deref : stl_slist_iterator[t] -> lvalue[t] = "*$1"; 383: fun begin : stl_slist[t]-> stl_slist_iterator[t]= "$1.begin()"; 384: fun end : stl_slist[t]-> stl_slist_iterator[t]= "$1.end()"; 385: proc erase : stl_slist[t] * stl_slist_iterator[t] = "$1.erase($1);"; 386: proc erase : stl_slist[t] * stl_slist_iterator[t] * stl_slist_iterator[t] = "$1.erase($1,$2);"; 387: proc clear : stl_slist[t] = "$1.clear();"; 388: proc pre_incr : lvalue[stl_slist_iterator[t]] = "++$1;"; 389: proc post_incr : stl_slist_iterator[t] = "++$1;"; 390: proc pre_decr : lvalue[stl_slist_iterator[t]] = "--$1;"; 391: proc post_decr : stl_slist_iterator[t] = "--$1;"; 392: proc push_front : stl_slist[t] * t = "$1.push_front($2);"; 393: fun front : stl_slist[t] -> t = "$1.front()"; 394: proc pop_front : stl_slist[t] = "$1.pop_back();"; 395: proc insert_after : stl_slist[t] * stl_slist_iterator[t] * t = "$1.insert_after($2,$3);"; 396: proc erase_after : stl_slist[t] * stl_slist_iterator[t] = "$1.erase_after($1);"; 397: } 398: // HASHTABLE based containers assume 399: // these classes will be added to C++ via TR1 in the future. 400: // g++ 3.2.2 at least has these classes 401: // The free SGI implementation may suffice as a replacement, 402: // this is what my version of g++ uses. 403: 404: module HashSet[t] 405: { 406: requires ext_hash_set; 407: type stl_hash_set = "__gnu_cxx::hash_set<?1>"; 408: type stl_hash_set_iterator = "__gnu_cxx::hash_set<?1>::iterator"; 409: type stl_hash_set_reverse_iterator = "__gnu_cxx::hash_set<?1>::reverse_iterator"; 410: fun create : unit -> stl_hash_set[t] = "(GXX_PARSER_HACK __gnu_cxx::hash_set<?1>())"; 411: gen_cmp stl_hash_set[t]; 412: fun len: stl_hash_set[t]->int = "$1.size()"; 413: fun empty: stl_hash_set[t]->int = "$1.empty()"; 414: gen_cmp stl_hash_set_iterator[t]; 415: gen_cmp stl_hash_set_reverse_iterator[t]; 416: proc pre_incr : lvalue[stl_hash_set_iterator[t]] = "++$1;"; 417: proc post_incr : stl_hash_set_iterator[t] = "++$1;"; 418: proc pre_incr : lvalue[stl_hash_set_reverse_iterator[t]] = "++$1;"; 419: proc post_incr : stl_hash_set_reverse_iterator[t] = "++$1;"; 420: proc pre_decr : lvalue[stl_hash_set_iterator[t]] = "--$1;"; 421: proc post_decr : stl_hash_set_iterator[t] = "--$1;"; 422: proc pre_decr: lvalue[stl_hash_set_reverse_iterator[t]] = "--$1;"; 423: proc post_decr : stl_hash_set_reverse_iterator[t] = "--$1;"; 424: fun deref : stl_hash_set_iterator[t] -> t = "*(#0*)&*$1:unary" is unary; 425: fun deref : stl_hash_set_reverse_iterator[t] -> t = "*(#0*)&*$1:unary" is unary; 426: fun begin : stl_hash_set[t]-> stl_hash_set_iterator[t]= "$1.begin()"; 427: fun end : stl_hash_set[t]-> stl_hash_set_iterator[t]= "$1.end()"; 428: fun rbegin : stl_hash_set[t]-> stl_hash_set_reverse_iterator[t]= "$1.rbegin()"; 429: fun rend : stl_hash_set[t]-> stl_hash_set_reverse_iterator[t]= "$1.rend()"; 430: proc insert : stl_hash_set[t] * t = "$1.insert($2);"; 431: proc erase : stl_hash_set[t] * stl_hash_set_iterator[t] = "$1.erase($1);"; 432: proc clear : stl_hash_set[t] = "$1.clear();"; 433: fun find : stl_hash_set[t] * t -> stl_hash_set_iterator[t] = "$1.find($2)"; 434: fun mem : stl_hash_set[t] * t -> bool = "$1.find($2) != $1.end()"; 435: } 436: module HashMultiSet[t] 437: { 438: requires ext_hash_set; 439: type stl_hash_multiset = "__gnu_cxx::hash_multiset<?1>"; 440: fun create : unit -> stl_hash_multiset[t] = "(GXX_PARSER_HACK __gnu_cxx::hash_multiset<?1>())"; 441: fun create : int * t -> stl_hash_multiset[t]= "(GXX_PARSER_HACK __gnu_cxx::hash_multiset<?1>($1,$2))"; 442: fun create[i] : i * i -> stl_hash_multiset[t] = "(GXX_PARSER_HACK __gnu_cxx::hash_multiset<?1>($1,$2))"; 443: gen_cmp stl_hash_multiset[t]; 444: fun len: stl_hash_multiset[t] -> int = "$1.size()"; 445: fun empty: stl_hash_multiset[t] -> int = "$1.empty()"; 446: type stl_hash_multiset_iterator = "__gnu_cxx::hash_multiset<?1>::iterator"; 447: gen_cmp stl_hash_multiset_iterator[t]; 448: gen_forward stl_hash_multiset_iterator[t]; 449: fun deref : stl_hash_multiset_iterator[t] -> lvalue[t] = "*$1"; 450: fun begin : stl_hash_multiset[t]-> stl_hash_multiset_iterator[t]= "$1.begin()"; 451: fun end : stl_hash_multiset[t]-> stl_hash_multiset_iterator[t]= "$1.end()"; 452: proc erase : stl_hash_multiset[t] * stl_hash_multiset_iterator[t] = "$1.erase($1);"; 453: proc erase : stl_hash_multiset[t] * stl_hash_multiset_iterator[t] * stl_hash_multiset_iterator[t] = "$1.erase($1,$2);"; 454: proc clear : stl_hash_multiset[t] = "$1.clear();"; 455: proc pre_incr : lvalue[stl_hash_multiset_iterator[t]] = "++$1;"; 456: proc post_incr : stl_hash_multiset_iterator[t] = "++$1;"; 457: proc pre_decr : lvalue[stl_hash_multiset_iterator[t]] = "--$1;"; 458: proc post_decr : stl_hash_multiset_iterator[t] = "--$1;"; 459: } 460: module HashMap[k,v] 461: { 462: requires ext_hash_map; 463: type stl_hash_map = "__gnu_cxx::hash_map<?1,?2>"; 464: type stl_hash_map_iterator = "__gnu_cxx::hash_map<?1,?2>::iterator"; 465: type stl_hash_map_reverse_iterator = "__gnu_cxx::hash_map<?1,?2>::reverse_iterator"; 466: fun create : unit -> stl_hash_map[k,v] = "(GXX_PARSER_HACK __gnu_cxx::hash_map<?1,?2>())"; 467: gen_cmp stl_hash_map[k,v]; 468: fun len: stl_hash_map[k,v]->int = "$1.size()"; 469: fun empty: stl_hash_map[k,v]->int = "$1.empty()"; 470: gen_cmp stl_hash_map_iterator[k,v]; 471: gen_cmp stl_hash_map_reverse_iterator[k,v]; 472: proc pre_incr : stl_hash_map_iterator[k,v] = "++$1;"; 473: proc post_incr : stl_hash_map_iterator[k,v] = "++$1;"; 474: proc pre_incr : stl_hash_map_reverse_iterator[k,v] = "++$1;"; 475: proc post_incr : stl_hash_map_reverse_iterator[k,v] = "++$1;"; 476: proc pre_decr : stl_hash_map_iterator[k,v] = "--$1;"; 477: proc post_decr : stl_hash_map_iterator[k,v] = "--$1;"; 478: proc pre_decr : stl_hash_map_reverse_iterator[k,v] = "--$1;"; 479: proc post_decr : stl_hash_map_reverse_iterator[k,v] = "--$1;"; 480: fun deref : stl_hash_map_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary; 481: fun begin : stl_hash_map[k,v]-> stl_hash_map_iterator[k,v]= "$1.begin()"; 482: fun end : stl_hash_map[k,v]-> stl_hash_map_iterator[k,v]= "$1.end()"; 483: fun deref : stl_hash_map_reverse_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary; 484: fun rbegin : stl_hash_map[k,v]-> stl_hash_map_reverse_iterator[k,v]= "$1.rbegin()"; 485: fun rend : stl_hash_map[k,v]-> stl_hash_map_reverse_iterator[k,v]= "$1.rend()"; 486: proc insert : stl_hash_map[k,v] * k * v = "$1.insert(std::make_pair($2,$3));"; 487: proc erase : stl_hash_map[k,v] * stl_hash_map_iterator[k,v] = "$1.erase($1);"; 488: proc clear : stl_hash_map[k,v] = "$1.clear();"; 489: fun find : stl_hash_map[k,v] * k -> stl_hash_map_iterator[k,v] = "$1.find($2)"; 490: fun mem : stl_hash_map[k,v] * k -> bool = "$1.find($2) != $1.end()"; 491: fun subscript: stl_hash_map[k,v] * k -> lvalue[v] = "$1[$2]"; 492: } 493: module HashMultiMap[k,v] 494: { 495: requires ext_hash_map; 496: type stl_hash_multimap = "__gnu_cxx::hash_multimap<?1,?2>"; 497: type stl_hash_multimap_iterator = "__gnu_cxx::hash_multimap<?1,?2>::iterator"; 498: type stl_hash_multimap_reverse_iterator = "__gnu_cxx::hash_multimap<?1,?2>::reverse_iterator"; 499: fun create : unit -> stl_hash_multimap[k,v] = "(GXX_PARSER_HACK __gnu_cxx::hash_multimap<?1,?2>())"; 500: gen_cmp stl_hash_multimap[k,v]; 501: fun len: stl_hash_multimap[k,v]->int = "$1.size()"; 502: fun empty: stl_hash_multimap[k,v]->int = "$1.empty()"; 503: gen_cmp stl_hash_multimap_iterator[k,v]; 504: gen_cmp stl_hash_multimap_reverse_iterator[k,v]; 505: proc pre_incr : stl_hash_multimap_iterator[k,v] = "++$1;"; 506: proc post_incr : stl_hash_multimap_iterator[k,v] = "++$1;"; 507: proc pre_incr : stl_hash_multimap_reverse_iterator[k,v] = "++$1;"; 508: proc post_incr : stl_hash_multimap_reverse_iterator[k,v] = "++$1;"; 509: proc pre_decr : stl_hash_multimap_iterator[k,v] = "--$1;"; 510: proc post_decr : stl_hash_multimap_iterator[k,v] = "--$1;"; 511: proc pre_decr : stl_hash_multimap_reverse_iterator[k,v] = "--$1;"; 512: proc post_decr : stl_hash_multimap_reverse_iterator[k,v] = "--$1;"; 513: fun deref : stl_hash_multimap_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary; 514: fun begin : stl_hash_multimap[k,v]-> stl_hash_multimap_iterator[k,v]= "$1.begin()"; 515: fun end : stl_hash_multimap[k,v]-> stl_hash_multimap_iterator[k,v]= "$1.end()"; 516: fun deref : stl_hash_multimap_reverse_iterator[k,v] -> k * lvalue[v] = "*(#0*)&*$1:unary" is unary; 517: fun rbegin : stl_hash_multimap[k,v]-> stl_hash_multimap_reverse_iterator[k,v]= "$1.rbegin()"; 518: fun rend : stl_hash_multimap[k,v]-> stl_hash_multimap_reverse_iterator[k,v]= "$1.rend()"; 519: proc insert : stl_hash_multimap[k,v] * k * v = "$1.insert(std::make_pair($2,$3));"; 520: proc erase : stl_hash_multimap[k,v] * stl_hash_multimap_iterator[k,v] = "$1.erase($1);"; 521: proc clear : stl_hash_multimap[k,v] = "$1.clear();"; 522: fun find : stl_hash_multimap[k,v] * k -> stl_hash_multimap_iterator[k,v] = "$1.find($2)"; 523: fun mem : stl_hash_multimap[k,v] * k -> bool = "$1.find($2) != $1.end()"; 524: fun subscript: stl_hash_multimap[k,v] * k -> lvalue[v] = "$1[$2]"; 525: } 526: }