profile/graph.svg

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
 "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<!-- Generated by graphviz version 2.43.0 (0)
 -->
<!-- Title: G Pages: 1 -->
<svg width="898pt" height="680pt"
 viewBox="0.00 0.00 897.51 679.96" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 675.96)">
<title>G</title>
<polygon fill="white" stroke="transparent" points="-4,4 -4,-675.96 893.51,-675.96 893.51,4 -4,4"/>
<!-- GCC -->
<g id="node1" class="node">
<title>GCC</title>
<ellipse fill="none" stroke="black" cx="506.5" cy="-570.09" rx="57.97" ry="26.74"/>
<text text-anchor="middle" x="506.5" y="-573.89" font-family="Times,serif" font-size="14.00">compiler,</text>
<text text-anchor="middle" x="506.5" y="-558.89" font-family="Times,serif" font-size="14.00">linker</text>
</g>
<!-- binary -->
<g id="node2" class="node">
<title>binary</title>
<polygon fill="none" stroke="black" points="554.5,-506.22 458.5,-506.22 458.5,-470.22 554.5,-470.22 554.5,-506.22"/>
<text text-anchor="middle" x="506.5" y="-484.52" font-family="Times,serif" font-size="14.00">ELF binary</text>
</g>
<!-- GCC&#45;&gt;binary -->
<g id="edge2" class="edge">
<title>GCC&#45;&gt;binary</title>
<path fill="none" stroke="black" d="M506.5,-542.94C506.5,-534.49 506.5,-525.11 506.5,-516.58"/>
<polygon fill="black" stroke="black" points="510,-516.37 506.5,-506.37 503,-516.37 510,-516.37"/>
</g>
<!-- BAP -->
<g id="node12" class="node">
<title>BAP</title>
<ellipse fill="none" stroke="black" cx="419.5" cy="-415.22" rx="30.59" ry="18"/>
<text text-anchor="middle" x="419.5" y="-411.52" font-family="Times,serif" font-size="14.00">BAP</text>
</g>
<!-- binary&#45;&gt;BAP -->
<g id="edge3" class="edge">
<title>binary&#45;&gt;BAP</title>
<path fill="none" stroke="black" d="M485.44,-470.03C473.15,-460 457.56,-447.28 444.63,-436.73"/>
<polygon fill="black" stroke="black" points="446.54,-433.77 436.57,-430.16 442.11,-439.19 446.54,-433.77"/>
</g>
<!-- readelf -->
<g id="node14" class="node">
<title>readelf</title>
<ellipse fill="none" stroke="black" cx="711.5" cy="-361.22" rx="43.59" ry="18"/>
<text text-anchor="middle" x="711.5" y="-357.52" font-family="Times,serif" font-size="14.00">readelf</text>
</g>
<!-- binary&#45;&gt;readelf -->
<g id="edge12" class="edge">
<title>binary&#45;&gt;readelf</title>
<path fill="none" stroke="black" d="M534.57,-470.1C572.42,-447.03 639.63,-406.04 679.43,-381.78"/>
<polygon fill="black" stroke="black" points="681.48,-384.62 688.2,-376.43 677.84,-378.65 681.48,-384.62"/>
</g>
<!-- C -->
<g id="node3" class="node">
<title>C</title>
<polygon fill="none" stroke="black" points="557,-671.96 456,-671.96 456,-633.96 557,-633.96 557,-671.96"/>
<text text-anchor="middle" x="506.5" y="-656.76" font-family="Times,serif" font-size="14.00">C</text>
<text text-anchor="middle" x="506.5" y="-641.76" font-family="Times,serif" font-size="14.00">source code</text>
</g>
<!-- C&#45;&gt;GCC -->
<g id="edge1" class="edge">
<title>C&#45;&gt;GCC</title>
<path fill="none" stroke="black" d="M506.5,-633.61C506.5,-625.75 506.5,-616.3 506.5,-607.14"/>
<polygon fill="black" stroke="black" points="510,-607.03 506.5,-597.03 503,-607.03 510,-607.03"/>
</g>
<!-- BIR -->
<g id="node4" class="node">
<title>BIR</title>
<polygon fill="none" stroke="black" points="497,-324.85 342,-324.85 342,-271.85 497,-271.85 497,-324.85"/>
<text text-anchor="middle" x="419.5" y="-309.65" font-family="Times,serif" font-size="14.00">BIR</text>
<text text-anchor="middle" x="419.5" y="-294.65" font-family="Times,serif" font-size="14.00">program semantics</text>
<text text-anchor="middle" x="419.5" y="-279.65" font-family="Times,serif" font-size="14.00">(human readable)</text>
</g>
<!-- ADT -->
<g id="node5" class="node">
<title>ADT</title>
<polygon fill="none" stroke="black" points="670,-324.85 515,-324.85 515,-271.85 670,-271.85 670,-324.85"/>
<text text-anchor="middle" x="592.5" y="-309.65" font-family="Times,serif" font-size="14.00">ADT</text>
<text text-anchor="middle" x="592.5" y="-294.65" font-family="Times,serif" font-size="14.00">program semantics</text>
<text text-anchor="middle" x="592.5" y="-279.65" font-family="Times,serif" font-size="14.00">(machine readable)</text>
</g>
<!-- BASIL -->
<g id="node6" class="node">
<title>BASIL</title>
<ellipse fill="none" stroke="black" cx="749.5" cy="-207.61" rx="140.01" ry="26.74"/>
<text text-anchor="middle" x="749.5" y="-211.41" font-family="Times,serif" font-size="14.00">BASIL</text>
<text text-anchor="middle" x="749.5" y="-196.41" font-family="Times,serif" font-size="14.00">(bil_to_boogie_translator)</text>
</g>
<!-- ADT&#45;&gt;BASIL -->
<g id="edge11" class="edge">
<title>ADT&#45;&gt;BASIL</title>
<path fill="none" stroke="black" d="M637.91,-271.68C656.36,-261.25 677.8,-249.14 696.92,-238.33"/>
<polygon fill="black" stroke="black" points="698.83,-241.27 705.81,-233.3 695.38,-235.18 698.83,-241.27"/>
</g>
<!-- annotated_boogie_program -->
<g id="node8" class="node">
<title>annotated_boogie_program</title>
<polygon fill="none" stroke="black" points="794,-143.74 705,-143.74 705,-90.74 794,-90.74 794,-143.74"/>
<text text-anchor="middle" x="749.5" y="-128.54" font-family="Times,serif" font-size="14.00">annotated</text>
<text text-anchor="middle" x="749.5" y="-113.54" font-family="Times,serif" font-size="14.00">Boogie</text>
<text text-anchor="middle" x="749.5" y="-98.54" font-family="Times,serif" font-size="14.00">program</text>
</g>
<!-- BASIL&#45;&gt;annotated_boogie_program -->
<g id="edge15" class="edge">
<title>BASIL&#45;&gt;annotated_boogie_program</title>
<path fill="none" stroke="black" d="M749.5,-180.57C749.5,-172.23 749.5,-162.84 749.5,-153.93"/>
<polygon fill="black" stroke="black" points="753,-153.79 749.5,-143.79 746,-153.79 753,-153.79"/>
</g>
<!-- specification -->
<g id="node7" class="node">
<title>specification</title>
<polygon fill="none" stroke="black" points="804.5,-324.85 688.5,-324.85 688.5,-271.85 810.5,-271.85 810.5,-318.85 804.5,-324.85"/>
<polyline fill="none" stroke="black" points="804.5,-324.85 804.5,-318.85 "/>
<polyline fill="none" stroke="black" points="810.5,-318.85 804.5,-318.85 "/>
<text text-anchor="middle" x="749.5" y="-309.65" font-family="Times,serif" font-size="14.00">rely/guarantee</text>
<text text-anchor="middle" x="749.5" y="-294.65" font-family="Times,serif" font-size="14.00">pre/post</text>
<text text-anchor="middle" x="749.5" y="-279.65" font-family="Times,serif" font-size="14.00">specifications</text>
</g>
<!-- specification&#45;&gt;BASIL -->
<g id="edge14" class="edge">
<title>specification&#45;&gt;BASIL</title>
<path fill="none" stroke="black" d="M749.5,-271.68C749.5,-263.29 749.5,-253.81 749.5,-244.8"/>
<polygon fill="black" stroke="black" points="753,-244.53 749.5,-234.53 746,-244.53 753,-244.53"/>
</g>
<!-- boogie -->
<g id="node9" class="node">
<title>boogie</title>
<ellipse fill="none" stroke="black" cx="749.5" cy="-26.87" rx="48.17" ry="26.74"/>
<text text-anchor="middle" x="749.5" y="-30.67" font-family="Times,serif" font-size="14.00">Boogie</text>
<text text-anchor="middle" x="749.5" y="-15.67" font-family="Times,serif" font-size="14.00">verifier</text>
</g>
<!-- annotated_boogie_program&#45;&gt;boogie -->
<g id="edge16" class="edge">
<title>annotated_boogie_program&#45;&gt;boogie</title>
<path fill="none" stroke="black" d="M749.5,-90.68C749.5,-82.4 749.5,-73.05 749.5,-64.15"/>
<polygon fill="black" stroke="black" points="753,-63.99 749.5,-53.99 746,-63.99 753,-63.99"/>
</g>
<!-- ASL -->
<g id="node10" class="node">
<title>ASL</title>
<polygon fill="none" stroke="black" points="165,-324.85 0,-324.85 0,-271.85 171,-271.85 171,-318.85 165,-324.85"/>
<polyline fill="none" stroke="black" points="165,-324.85 165,-318.85 "/>
<polyline fill="none" stroke="black" points="171,-318.85 165,-318.85 "/>
<text text-anchor="middle" x="85.5" y="-309.65" font-family="Times,serif" font-size="14.00">ASL</text>
<text text-anchor="middle" x="85.5" y="-294.65" font-family="Times,serif" font-size="14.00">instruction semantics</text>
<text text-anchor="middle" x="85.5" y="-279.65" font-family="Times,serif" font-size="14.00">specifications</text>
</g>
<!-- ASLi -->
<g id="node13" class="node">
<title>ASLi</title>
<ellipse fill="none" stroke="black" cx="256.5" cy="-207.61" rx="32.49" ry="18"/>
<text text-anchor="middle" x="256.5" y="-203.91" font-family="Times,serif" font-size="14.00">ASLi</text>
</g>
<!-- ASL&#45;&gt;ASLi -->
<g id="edge7" class="edge">
<title>ASL&#45;&gt;ASLi</title>
<path fill="none" stroke="black" d="M134.96,-271.68C163.82,-256.7 199.39,-238.25 224.58,-225.18"/>
<polygon fill="black" stroke="black" points="226.42,-228.16 233.68,-220.45 223.2,-221.95 226.42,-228.16"/>
</g>
<!-- ASLp -->
<g id="node11" class="node">
<title>ASLp</title>
<ellipse fill="none" stroke="black" cx="256.5" cy="-298.35" rx="67.76" ry="26.74"/>
<text text-anchor="middle" x="256.5" y="-302.15" font-family="Times,serif" font-size="14.00">ASLp,</text>
<text text-anchor="middle" x="256.5" y="-287.15" font-family="Times,serif" font-size="14.00">BAP plugin</text>
</g>
<!-- ASLp&#45;&gt;BAP -->
<g id="edge10" class="edge">
<title>ASLp&#45;&gt;BAP</title>
<path fill="none" stroke="black" d="M253.05,-325.53C252.29,-342.87 254.47,-364.96 267.5,-379.22 282.38,-395.49 339.82,-405.22 379.66,-410.15"/>
<polygon fill="black" stroke="black" points="379.29,-413.63 389.63,-411.33 380.11,-406.68 379.29,-413.63"/>
<text text-anchor="middle" x="307" y="-365.02" font-family="Times,serif" font-size="14.00">instruction</text>
<text text-anchor="middle" x="307" y="-350.02" font-family="Times,serif" font-size="14.00">semantics</text>
</g>
<!-- ASLp&#45;&gt;ASLi -->
<g id="edge8" class="edge">
<title>ASLp&#45;&gt;ASLi</title>
<path fill="none" stroke="black" d="M250.28,-271.21C249.59,-260.05 249.57,-247.03 250.22,-235.76"/>
<polygon fill="black" stroke="black" points="253.73,-235.87 251.05,-225.62 246.75,-235.3 253.73,-235.87"/>
</g>
<!-- BAP&#45;&gt;BIR -->
<g id="edge4" class="edge">
<title>BAP&#45;&gt;BIR</title>
<path fill="none" stroke="black" d="M419.5,-396.77C419.5,-380.53 419.5,-355.8 419.5,-335.33"/>
<polygon fill="black" stroke="black" points="423,-335.08 419.5,-325.08 416,-335.08 423,-335.08"/>
</g>
<!-- BAP&#45;&gt;ADT -->
<g id="edge5" class="edge">
<title>BAP&#45;&gt;ADT</title>
<path fill="none" stroke="black" d="M439.01,-401.27C464.59,-384.28 510.31,-353.93 545.22,-330.75"/>
<polygon fill="black" stroke="black" points="547.44,-333.47 553.84,-325.02 543.57,-327.64 547.44,-333.47"/>
</g>
<!-- BAP&#45;&gt;ASLp -->
<g id="edge6" class="edge">
<title>BAP&#45;&gt;ASLp</title>
<path fill="none" stroke="black" d="M407.12,-398.48C394.26,-382.91 372.91,-359.16 350.5,-343.22 339.16,-335.16 326.11,-327.97 313.4,-321.85"/>
<polygon fill="black" stroke="black" points="314.79,-318.64 304.25,-317.6 311.84,-324.99 314.79,-318.64"/>
</g>
<!-- ASLi&#45;&gt;ASLp -->
<g id="edge9" class="edge">
<title>ASLi&#45;&gt;ASLp</title>
<path fill="none" stroke="black" d="M261.95,-225.62C263.06,-235.69 263.46,-248.86 263.15,-261.16"/>
<polygon fill="black" stroke="black" points="259.65,-261.06 262.72,-271.21 266.64,-261.36 259.65,-261.06"/>
</g>
<!-- readelf&#45;&gt;BASIL -->
<g id="edge13" class="edge">
<title>readelf&#45;&gt;BASIL</title>
<path fill="none" stroke="black" d="M754.37,-358.02C777.66,-354.38 804.66,-345.63 819.5,-325.22 833.55,-305.9 829.23,-293.29 819.5,-271.48 814.25,-259.71 805.59,-249.22 796.11,-240.34"/>
<polygon fill="black" stroke="black" points="798.22,-237.53 788.39,-233.58 793.6,-242.8 798.22,-237.53"/>
<text text-anchor="middle" x="850.5" y="-294.65" font-family="Times,serif" font-size="14.00">stdout</text>
</g>
</g>
</svg>