===========================================================
.___ __ __
_________________ __ __ __| _/|__|/ |_
/ ___\_` __ \__ \ | | \/ __ | | \\_ __\
/ /_/ > | \// __ \| | / /_/ | | || |
\___ /|__| (____ /____/\____ | |__||__|
/_____/ \/ \/
grep rough audit - static analysis tool
v2.8 written by @Wireghoul
=================================[justanotherhacker.com]===
dafny-2.3.0+dfsg/Docs/DafnyRef/DafnyRef.mdk-7910-
dafny-2.3.0+dfsg/Docs/DafnyRef/DafnyRef.mdk:7911:* `{:$}`
dafny-2.3.0+dfsg/Docs/DafnyRef/DafnyRef.mdk:7912:* `{:$renamed$}`
dafny-2.3.0+dfsg/Docs/DafnyRef/DafnyRef.mdk-7913-* `{:InlineAssume}`
##############################################
dafny-2.3.0+dfsg/Docs/DafnyRef/out/DafnyRef.html-3006-\]</desc><g id='math-023b8b'><use x='196.157' xlink:href='#g3-102' y='34.996'/><use x='213.176' xlink:href='#g5-61' y='34.996'/><use x='231.994' xlink:href='#g1-70' y='34.996'/><use x='240.144' xlink:href='#g5-40' y='34.996'/><use x='244.019' xlink:href='#g3-102' y='34.996'/><use x='249.969' xlink:href='#g5-41' y='34.996'/></g></svg></div></div>
dafny-2.3.0+dfsg/Docs/DafnyRef/out/DafnyRef.html:3007:<p class="p noindent para-continued" data-line="2804"><span data-line="2804"></span>where <span data-line="2804"></span><svg class="math-inline math-render-svg math" style="vertical-align:-0.0210em;height:0.7981em;width:0.9100em" viewBox='-0.199 25.92 8.667 7.601' ><desc>$\mathcal{F}$</desc><g id='math-a86b47'><use x='0' xlink:href='#g1-70' y='33.004'/></g></svg><span data-line="2804"></span> is a non-recursive function of type
dafny-2.3.0+dfsg/Docs/DafnyRef/out/DafnyRef.html-3008-<span data-line="2805"></span><svg class="math-inline math-render-svg math" style="vertical-align:-0.2930em;height:1.0879em;width:9.3152em" viewBox='-18.199 25.332 88.716 10.361' ><desc>$(X \to Y) \to X \to Y$</desc><g id='math-8112dc'><use x='-18' xlink:href='#g5-40' y='33.004'/><use x='-14.126' xlink:href='#g3-88' y='33.004'/><use x='-2.323' xlink:href='#g1-33' y='33.004'/><use x='10.407' xlink:href='#g3-89' y='33.004'/><use x='18.405' xlink:href='#g5-41' y='33.004'/><use x='25.047' xlink:href='#g1-33' y='33.004'/><use x='37.777' xlink:href='#g3-88' y='33.004'/><use x='49.58' xlink:href='#g1-33' y='33.004'/><use x='62.31' xlink:href='#g3-89' y='33.004'/></g></svg><span data-line="2805"></span>. Because it takes a function as an argument,
##############################################
dafny-2.3.0+dfsg/Docs/DafnyRef/out/DafnyRef.html-3101-<p class="p indent para-continue" data-line="2904"><span data-line="2904"></span>For any complete lattice <span data-line="2904"></span><svg class="math-inline math-render-svg math" style="vertical-align:-0.2930em;height:1.0879em;width:2.8005em" viewBox='-0.199 25.332 26.671 10.361' ><desc>$(Y,\leq)$</desc><g id='math-3057ef'><use x='0' xlink:href='#g5-40' y='33.004'/><use x='3.874' xlink:href='#g3-89' y='33.004'/><use x='10.212' xlink:href='#g3-59' y='33.004'/><use x='14.64' xlink:href='#g1-20' y='33.004'/><use x='22.388' xlink:href='#g5-41' y='33.004'/></g></svg><span data-line="2904"></span> and any set <span data-line="2904"></span><svg class="math-inline math-render-svg math" style="vertical-align:-0.0210em;height:0.7563em;width:0.9916em" viewBox='-18.199 26 9.444 7.203' ><desc>$X$</desc><g id='math-02129b'><use x='-18' xlink:href='#g3-88' y='33.004'/></g></svg><span data-line="2904"></span>, we can by <span data-line="2904"></span><em class="em-low1">pointwise extension</em><span data-line="2904"></span> define
dafny-2.3.0+dfsg/Docs/DafnyRef/out/DafnyRef.html:3102:a complete lattice <span data-line="2905"></span><svg class="math-inline math-render-svg math" style="vertical-align:-0.2930em;height:1.0879em;width:6.7711em" viewBox='-0.199 25.332 64.487 10.361' ><desc>$(X \to Y, \FBelow)$</desc><g id='math-872794'><use x='0' xlink:href='#g5-40' y='33.004'/><use x='3.874' xlink:href='#g3-88' y='33.004'/><use x='15.677' xlink:href='#g1-33' y='33.004'/><use x='28.407' xlink:href='#g3-89' y='33.004'/><use x='34.745' xlink:href='#g3-59' y='33.004'/><use x='48.305' xlink:href='#g5-95' y='33.004'/><use x='44.707' xlink:href='#g1-41' y='33.004'/><use x='60.204' xlink:href='#g5-41' y='33.004'/></g></svg><span data-line="2905"></span>, where for any <span data-line="2905"></span><svg class="math-inline math-render-svg math" style="vertical-align:-0.2384em;height:0.9938em;width:5.7821em" viewBox='-18.199 25.781 55.068 9.465' ><desc>$f,g \colon X \to Y$</desc><g id='math-86cb35'><use x='-18' xlink:href='#g3-102' y='33.004'/><use x='-12.604' xlink:href='#g3-59' y='33.004'/><use x='-8.176' xlink:href='#g3-103' y='33.004'/><use x='-1.959' xlink:href='#g5-58' y='33.004'/><use x='4.129' xlink:href='#g3-88' y='33.004'/><use x='15.932' xlink:href='#g1-33' y='33.004'/><use x='28.662' xlink:href='#g3-89' y='33.004'/></g></svg><span data-line="2905"></span>,
dafny-2.3.0+dfsg/Docs/DafnyRef/out/DafnyRef.html-3103-</p>
##############################################
dafny-2.3.0+dfsg/Docs/DafnyRef/out/DafnyRef.html-3134-<p class="p indent para-continue" data-line="2936"><span data-line="2936"></span>Let me introduce a running example. Consider the following equation,
dafny-2.3.0+dfsg/Docs/DafnyRef/out/DafnyRef.html:3135:where <span data-line="2937"></span><svg class="math-inline math-render-svg math" style="vertical-align:-0.0210em;height:0.5158em;width:0.6407em" viewBox='-0.199 28.401 6.102 4.912' ><desc>$x$</desc><g id='math-9dd4e4'><use x='0' xlink:href='#g3-120' y='33.004'/></g></svg><span data-line="2937"></span> ranges over the integers:
dafny-2.3.0+dfsg/Docs/DafnyRef/out/DafnyRef.html-3136-</p>
##############################################
dafny-2.3.0+dfsg/Docs/DafnyRef/out/DafnyRef.html-3220-functions, <span data-line="3031"></span><svg class="math-inline math-render-svg math" style="vertical-align:-0.2873em;height:1.2336em;width:1.3988em" viewBox='-0.199 23.959 13.322 11.749' ><desc>$\iter{f}_k$</desc><g id='math-8b50b1'><use x='0' xlink:href='#g4-91' y='29.388'/><use x='2.062' xlink:href='#g3-102' y='33.004'/><use x='8.012' xlink:href='#g4-107' y='35.439'/></g></svg><span data-line="3031"></span> and <span data-line="3031"></span><svg class="math-inline math-render-svg math" style="vertical-align:-0.2912em;height:1.2088em;width:1.3988em" viewBox='-0.199 24.196 13.322 11.512' ><desc>$\Iter{f}_k$</desc><g id='math-798979'><use x='0' xlink:href='#g4-93' y='29.388'/><use x='2.062' xlink:href='#g3-102' y='33.004'/><use x='8.012' xlink:href='#g4-107' y='35.439'/></g></svg><span data-line="3031"></span>
dafny-2.3.0+dfsg/Docs/DafnyRef/out/DafnyRef.html:3221:where <span data-line="3032"></span><svg class="math-inline math-render-svg math" style="vertical-align:-0.0210em;height:0.7793em;width:0.6204em" viewBox='-18.199 25.89 5.909 7.422' ><desc>$k$</desc><g id='math-8ce4b1'><use x='-18' xlink:href='#g3-107' y='33.004'/></g></svg><span data-line="3032"></span> ranges over the natural numbers:
dafny-2.3.0+dfsg/Docs/DafnyRef/out/DafnyRef.html-3222-</p>
##############################################
dafny-2.3.0+dfsg/Source/Dafny/DafnyMain.cs-44- Assembly.ReflectionOnlyLoad("DafnyRuntime");
dafny-2.3.0+dfsg/Source/Dafny/DafnyMain.cs:45: var asm = Assembly.ReflectionOnlyLoadFrom(filePath);
dafny-2.3.0+dfsg/Source/Dafny/DafnyMain.cs-46- string sourceText = null;
##############################################
dafny-2.3.0+dfsg/Test/wishlist/sequences-literals.dfy-29- } else if * {
dafny-2.3.0+dfsg/Test/wishlist/sequences-literals.dfy:30: // This also works, thanks to the magic of triggering on `$Box`.
dafny-2.3.0+dfsg/Test/wishlist/sequences-literals.dfy-31- assert exists n {:autotriggers false} :: n in s;
##############################################
dafny-2.3.0+dfsg/Test/wishlist/sequences-literals.dfy-50- } else if * {
dafny-2.3.0+dfsg/Test/wishlist/sequences-literals.dfy:51: // This works: this is certainly more `triggering-on-$Box` magic, but I'm
dafny-2.3.0+dfsg/Test/wishlist/sequences-literals.dfy-52- // not sure exactly how it works
##############################################
dafny-2.3.0+dfsg/Test/wishlist/sequences-literals.dfy-54- } else if * {
dafny-2.3.0+dfsg/Test/wishlist/sequences-literals.dfy:55: // `$Box` only offers limited solace, though
dafny-2.3.0+dfsg/Test/wishlist/sequences-literals.dfy-56- assert exists n {:autotriggers false} :: n in s && n < 3;