@@ -279,62 +279,37 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
279
279
graphml.set_attribute (" xmlns:xsi" , " http://www.w3.org/2001/XMLSchema-instance" );
280
280
graphml.set_attribute (" xmlns" , " http://graphml.graphdrawing.org/xmlns" );
281
281
282
- // <key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
283
- {
284
- xmlt &key=graphml.new_element (" key" );
285
- key.set_attribute (" attr.name" , " assumption" );
286
- key.set_attribute (" attr.type" , " string" );
287
- key.set_attribute (" for" , " edge" );
288
- key.set_attribute (" id" , " assumption" );
289
- }
290
-
291
- // <key attr.name="sourcecode" attr.type="string" for="edge" id="sourcecode"/>
282
+ // <key attr.name="originFileName" attr.type="string" for="edge"
283
+ // id="originfile">
284
+ // <default>"<command-line>"</default>
285
+ // </key>
292
286
{
293
287
xmlt &key=graphml.new_element (" key" );
294
- key.set_attribute (" attr.name" , " sourcecode " );
288
+ key.set_attribute (" attr.name" , " originFileName " );
295
289
key.set_attribute (" attr.type" , " string" );
296
290
key.set_attribute (" for" , " edge" );
297
- key.set_attribute (" id" , " sourcecode" );
298
- }
291
+ key.set_attribute (" id" , " originfile" );
299
292
300
- // <key attr.name="sourcecodeLanguage" attr.type="string" for="graph" id="sourcecodelang"/>
301
- {
302
- xmlt &key=graphml.new_element (" key" );
303
- key.set_attribute (" attr.name" , " sourcecodeLanguage" );
304
- key.set_attribute (" attr.type" , " string" );
305
- key.set_attribute (" for" , " graph" );
306
- key.set_attribute (" id" , " sourcecodelang" );
293
+ key.new_element (" default" ).data =" <command-line>" ;
307
294
}
308
295
309
- // <key attr.name="control " attr.type="string" for="edge " id="control "/>
296
+ // <key attr.name="invariant " attr.type="string" for="node " id="invariant "/>
310
297
{
311
298
xmlt &key=graphml.new_element (" key" );
312
- key.set_attribute (" attr.name" , " control " );
299
+ key.set_attribute (" attr.name" , " invariant " );
313
300
key.set_attribute (" attr.type" , " string" );
314
- key.set_attribute (" for" , " edge" );
315
- key.set_attribute (" id" , " control" );
316
- }
317
-
318
- // <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
319
- {
320
- xmlt &key=graphml.new_element (" key" );
321
- key.set_attribute (" attr.name" , " startline" );
322
- key.set_attribute (" attr.type" , " int" );
323
- key.set_attribute (" for" , " edge" );
324
- key.set_attribute (" id" , " startline" );
301
+ key.set_attribute (" for" , " node" );
302
+ key.set_attribute (" id" , " invariant" );
325
303
}
326
304
327
- // <key attr.name="originFileName" attr.type="string" for="edge" id="originfile">
328
- // <default>"<command-line>"</default>
329
- // </key>
305
+ // <key attr.name="invariant.scope" attr.type="string" for="node"
306
+ // id="invariant.scope"/>
330
307
{
331
308
xmlt &key=graphml.new_element (" key" );
332
- key.set_attribute (" attr.name" , " originFileName " );
309
+ key.set_attribute (" attr.name" , " invariant.scope " );
333
310
key.set_attribute (" attr.type" , " string" );
334
- key.set_attribute (" for" , " edge" );
335
- key.set_attribute (" id" , " originfile" );
336
-
337
- key.new_element (" default" ).data =" <command-line>" ;
311
+ key.set_attribute (" for" , " node" );
312
+ key.set_attribute (" id" , " invariant.scope" );
338
313
}
339
314
340
315
// <key attr.name="nodeType" attr.type="string" for="node" id="nodetype">
@@ -350,7 +325,8 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
350
325
key.new_element (" default" ).data =" path" ;
351
326
}
352
327
353
- // <key attr.name="isFrontierNode" attr.type="boolean" for="node" id="frontier">
328
+ // <key attr.name="isFrontierNode" attr.type="boolean" for="node"
329
+ // id="frontier">
354
330
// <default>false</default>
355
331
// </key>
356
332
{
@@ -363,7 +339,8 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
363
339
key.new_element (" default" ).data =" false" ;
364
340
}
365
341
366
- // <key attr.name="isViolationNode" attr.type="boolean" for="node" id="violation">
342
+ // <key attr.name="isViolationNode" attr.type="boolean" for="node"
343
+ // id="violation">
367
344
// <default>false</default>
368
345
// </key>
369
346
{
@@ -402,7 +379,150 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
402
379
key.new_element (" default" ).data =" false" ;
403
380
}
404
381
405
- // <key attr.name="enterFunction" attr.type="string" for="edge" id="enterFunction"/>
382
+ // <key attr.name="enterLoopHead" attr.type="boolean" for="edge"
383
+ // id="enterLoopHead">
384
+ // <default>false</default>
385
+ // </key>
386
+ {
387
+ xmlt &key=graphml.new_element (" key" );
388
+ key.set_attribute (" attr.name" , " enterLoopHead" );
389
+ key.set_attribute (" attr.type" , " boolean" );
390
+ key.set_attribute (" for" , " edge" );
391
+ key.set_attribute (" id" , " enterLoopHead" );
392
+
393
+ key.new_element (" default" ).data =" false" ;
394
+ }
395
+
396
+ // <key attr.name="threadId" attr.type="string" for="edge" id="threadId"/>
397
+ // TODO: format for multi-threaded programs not defined yet
398
+ {
399
+ xmlt &key=graphml.new_element (" key" );
400
+ key.set_attribute (" attr.name" , " threadNumber" );
401
+ key.set_attribute (" attr.type" , " int" );
402
+ key.set_attribute (" for" , " node" );
403
+ key.set_attribute (" id" , " thread" );
404
+
405
+ key.new_element (" default" ).data =" 0" ;
406
+ }
407
+
408
+ // <key attr.name="sourcecodeLanguage" attr.type="string" for="graph"
409
+ // id="sourcecodelang"/>
410
+ {
411
+ xmlt &key=graphml.new_element (" key" );
412
+ key.set_attribute (" attr.name" , " sourcecodeLanguage" );
413
+ key.set_attribute (" attr.type" , " string" );
414
+ key.set_attribute (" for" , " graph" );
415
+ key.set_attribute (" id" , " sourcecodelang" );
416
+ }
417
+
418
+ // <key attr.name="programFile" attr.type="string" for="graph"
419
+ // id="programfile"/>
420
+ {
421
+ xmlt &key=graphml.new_element (" key" );
422
+ key.set_attribute (" attr.name" , " programFile" );
423
+ key.set_attribute (" attr.type" , " string" );
424
+ key.set_attribute (" for" , " graph" );
425
+ key.set_attribute (" id" , " programfile" );
426
+ }
427
+
428
+ // <key attr.name="programHash" attr.type="string" for="graph"
429
+ // id="programhash"/>
430
+ {
431
+ xmlt &key=graphml.new_element (" key" );
432
+ key.set_attribute (" attr.name" , " programHash" );
433
+ key.set_attribute (" attr.type" , " string" );
434
+ key.set_attribute (" for" , " graph" );
435
+ key.set_attribute (" id" , " programhash" );
436
+ }
437
+
438
+ // <key attr.name="specification" attr.type="string" for="graph"
439
+ // id="specification"/>
440
+ {
441
+ xmlt &key=graphml.new_element (" key" );
442
+ key.set_attribute (" attr.name" , " specification" );
443
+ key.set_attribute (" attr.type" , " string" );
444
+ key.set_attribute (" for" , " graph" );
445
+ key.set_attribute (" id" , " specification" );
446
+ }
447
+
448
+ // <key attr.name="architecture" attr.type="string" for="graph"
449
+ // id="architecture"/>
450
+ {
451
+ xmlt &key=graphml.new_element (" key" );
452
+ key.set_attribute (" attr.name" , " architecture" );
453
+ key.set_attribute (" attr.type" , " string" );
454
+ key.set_attribute (" for" , " graph" );
455
+ key.set_attribute (" id" , " architecture" );
456
+ }
457
+
458
+ // <key attr.name="producer" attr.type="string" for="graph"
459
+ // id="producer"/>
460
+ {
461
+ xmlt &key=graphml.new_element (" key" );
462
+ key.set_attribute (" attr.name" , " producer" );
463
+ key.set_attribute (" attr.type" , " string" );
464
+ key.set_attribute (" for" , " graph" );
465
+ key.set_attribute (" id" , " producer" );
466
+ }
467
+
468
+ // <key attr.name="sourcecode" attr.type="string" for="edge" id="sourcecode"/>
469
+ {
470
+ xmlt &key=graphml.new_element (" key" );
471
+ key.set_attribute (" attr.name" , " sourcecode" );
472
+ key.set_attribute (" attr.type" , " string" );
473
+ key.set_attribute (" for" , " edge" );
474
+ key.set_attribute (" id" , " sourcecode" );
475
+ }
476
+
477
+ // <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
478
+ {
479
+ xmlt &key=graphml.new_element (" key" );
480
+ key.set_attribute (" attr.name" , " startline" );
481
+ key.set_attribute (" attr.type" , " int" );
482
+ key.set_attribute (" for" , " edge" );
483
+ key.set_attribute (" id" , " startline" );
484
+ }
485
+
486
+ // <key attr.name="control" attr.type="string" for="edge" id="control"/>
487
+ {
488
+ xmlt &key=graphml.new_element (" key" );
489
+ key.set_attribute (" attr.name" , " control" );
490
+ key.set_attribute (" attr.type" , " string" );
491
+ key.set_attribute (" for" , " edge" );
492
+ key.set_attribute (" id" , " control" );
493
+ }
494
+
495
+ // <key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
496
+ {
497
+ xmlt &key=graphml.new_element (" key" );
498
+ key.set_attribute (" attr.name" , " assumption" );
499
+ key.set_attribute (" attr.type" , " string" );
500
+ key.set_attribute (" for" , " edge" );
501
+ key.set_attribute (" id" , " assumption" );
502
+ }
503
+
504
+ // <key attr.name="assumption.resultfunction" attr.type="string" for="edge"
505
+ // id="assumption.resultfunction"/>
506
+ {
507
+ xmlt &key=graphml.new_element (" key" );
508
+ key.set_attribute (" attr.name" , " assumption.resultfunction" );
509
+ key.set_attribute (" attr.type" , " string" );
510
+ key.set_attribute (" for" , " edge" );
511
+ key.set_attribute (" id" , " assumption.resultfunction" );
512
+ }
513
+
514
+ // <key attr.name="assumption.scope" attr.type="string" for="edge"
515
+ // id="assumption.scope"/>
516
+ {
517
+ xmlt &key=graphml.new_element (" key" );
518
+ key.set_attribute (" attr.name" , " assumption.scope" );
519
+ key.set_attribute (" attr.type" , " string" );
520
+ key.set_attribute (" for" , " edge" );
521
+ key.set_attribute (" id" , " assumption.scope" );
522
+ }
523
+
524
+ // <key attr.name="enterFunction" attr.type="string" for="edge"
525
+ // id="enterFunction"/>
406
526
{
407
527
xmlt &key=graphml.new_element (" key" );
408
528
key.set_attribute (" attr.name" , " enterFunction" );
@@ -411,7 +531,8 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
411
531
key.set_attribute (" id" , " enterFunction" );
412
532
}
413
533
414
- // <key attr.name="returnFromFunction" attr.type="string" for="edge" id="returnFrom"/>
534
+ // <key attr.name="returnFromFunction" attr.type="string" for="edge"
535
+ // id="returnFrom"/>
415
536
{
416
537
xmlt &key=graphml.new_element (" key" );
417
538
key.set_attribute (" attr.name" , " returnFromFunction" );
@@ -420,17 +541,16 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
420
541
key.set_attribute (" id" , " returnFrom" );
421
542
}
422
543
544
+ // <key attr.name="witness-type" attr.type="string" for="graph"
545
+ // id="witness-type"/>
423
546
{
424
547
xmlt &key=graphml.new_element (" key" );
425
- key.set_attribute (" attr.name" , " threadNumber" );
426
- key.set_attribute (" attr.type" , " int" );
427
- key.set_attribute (" for" , " node" );
428
- key.set_attribute (" id" , " thread" );
429
-
430
- key.new_element (" default" ).data =" 0" ;
548
+ key.set_attribute (" attr.name" , " witness-type" );
549
+ key.set_attribute (" attr.type" , " string" );
550
+ key.set_attribute (" for" , " graph" );
551
+ key.set_attribute (" id" , " witness-type" );
431
552
}
432
553
433
-
434
554
xmlt &graph=graphml.new_element (" graph" );
435
555
graph.set_attribute (" edgedefault" , " directed" );
436
556
0 commit comments