From 943f42cf7de3618910527a14b63e51f8216f649e Mon Sep 17 00:00:00 2001
From: Blinningjr <nicke.l@telia.com>
Date: Tue, 15 Dec 2020 16:57:38 +0100
Subject: [PATCH] Fixed get_sign.c based on marks feedback
---
examples/a.out | Bin 17488 -> 16616 bytes
examples/get_sign.bc | Bin 3004 -> 3008 bytes
examples/get_sign.c | 6 +--
examples/klee-last | 2 +-
examples/klee-out-1/assembly.ll | 60 +++++++++++++++++++++++++++
examples/klee-out-1/info | 22 ++++++++++
examples/klee-out-1/messages.txt | 1 +
examples/klee-out-1/run.istats | 52 +++++++++++++++++++++++
examples/klee-out-1/run.stats | Bin 0 -> 8192 bytes
examples/klee-out-1/test000001.ktest | Bin 0 -> 53 bytes
examples/klee-out-1/test000002.ktest | Bin 0 -> 53 bytes
examples/klee-out-1/test000003.ktest | Bin 0 -> 53 bytes
examples/klee-out-1/warnings.txt | 0
13 files changed, 139 insertions(+), 4 deletions(-)
create mode 100644 examples/klee-out-1/assembly.ll
create mode 100644 examples/klee-out-1/info
create mode 100644 examples/klee-out-1/messages.txt
create mode 100644 examples/klee-out-1/run.istats
create mode 100644 examples/klee-out-1/run.stats
create mode 100644 examples/klee-out-1/test000001.ktest
create mode 100644 examples/klee-out-1/test000002.ktest
create mode 100644 examples/klee-out-1/test000003.ktest
create mode 100644 examples/klee-out-1/warnings.txt
diff --git a/examples/a.out b/examples/a.out
index 81e51b36cd97f40e411fa57ab58a740248bba2d7..d17f0345c7afb7865dc5550d6d6c6a1db5cd5fa0 100755
GIT binary patch
delta 1014
zcmcc6!T6$)ae{{U3QGn!aA2@t;AU`OkY$kBXg`%nWa^O*Kg>Qgw>-R`dATWXYf$0Q
z^rMqsFhxubuwj|(!Ynd5z?6kiVX`BW@FaVd$tBF9ljk!l8OF!wWF{rY7ndX!mBi;J
zX67;EWF}?jq^1Uy=9Q!tm*^Ge>lx}9fJBo)Y_rLCm=zekH~(dp))F*@I))KSdvDg%
z6JatlG|)5BGtf0OE=?-UD=9V9RDg&ugo61B$vKI6=?Z13Ma7x<c?yPxdIow1x<->7
znG`p-7=<uR4ltFF^kQIOU}Rusc){cVHe3NrGBAWp4m1^)jAvkAU}E59Xb^zNLM0gz
zCpVgkOO`-oKcLBWP2OlKE;$WsvM>XO9je~FlOLLjOP&PF3NbLC$-V&D%Lule@$+Oy
zGyQr-u&;$M%n@P)xm<)n0L=txsCsmh^}yl+3>*rm?r{X0BgVksfGQr&$iN`Pz$?U{
zAOw+Mh5CNRWJYsw$#g~r1_1_f1_Ly0iIWY@#ToM^A2b(d?46uwE-pC@s!{<><>JW`
z&BY}*F)}a+GKn*2pvmqBnIL%yB+J0hzyNhL3)Bq{Cx0{-m*fSTEWu!bruXAyMGNuz
zIS>ypI6$LEAF7v=3FLAK43~>Cfj!JnAPDiV1ysEh6U2q+K79=`pNX4+0ct)}IRk@!
zX>pN$l22xyzMh_bPG*vRdUCRUg@swXnTc*rW?pH9ZhBs+zM%m~T2Bu|Vn`+zl^E*f
zGsMRyCS}H#B&JW^VByGUF!_Ro*k*3aI;P1<Ebf~HY!uiST_zhk$xqzCGI@%#h-ifY
n)D3J9TAG1@L3i?AXKk(uGl+;9)8tRiW}Ne&eq)~e(ODh<mP4&k
delta 1570
zcmaFS$atZHae{{U1#1R4aA2@t;AU`OP-0NrXg`%n<n$_;Bh`UwGc02F?_vJf_`_=#
z<Fv^ym?9XRCp$8Wvx+k?FeprRWD;gnn_S2&A)1q!l%12B8dREBl3HA%SDdeBsAn*_
zgIQTRCo?G-#5ZGzj|Z{ii%SxVO5$@9GxH|jVOC(Y-29hWT5Ga|g8-xDW=%a2rg}>~
zBRxZ1%hIIMypmEQO$9Jt!N|bS($K)bf+0C4F)v-AEVZaOGe1wkQqMroK-Wk?qa-oC
zSU<?s$JH^|HQv&|KtC-rFEK}xp^kxpfd%YM4n`2g!=MkM7#J9=7#J7~1RcP<3I+xS
zCJ3jVfx(`Efq^kB7esPYF)%PNGfk|hhw~U%3ZS|yKw@Da6^z0ll9g#<MI%T|6vSg-
zD`Q|_U}a%o6l7H86J}-R6A+i?6J!)(V_;y?V+1iAB$)ZExUIR>B|U}hB^el)Ss9q>
zp<<rG3=Ax&${>nZO&FMv)Uc^AF!R}Qb8|B=Fr<S$s|0caBjayAUIs=+Mv$)=85kHD
z(o;*~i!;;n^pe3|X5fT+n1Mlxm7A-Sm6OejEuEFSeh-AThn2CEl_8T=g6kP8E1MUq
zC>uvQD-W9uD{BN38v`RFiSdAByM9J~ZmND>W_C_uvA#=cadt_5fxe5mfsui$es+#l
zYHEB*X-R%jW@3(hYDHphK~8Eh-0=*Vc_j>>#KTa*kT}_qNpbTOgAk_46AaiGr6xNv
zi83=YNJD8EC@l-6<tAS@(q!bBY-lVl$p?yW2402@0+9HJga`wJ;^ahQaY=Jf05V80
z7&t&=K|u&o;Wl}qvA85CT`)25GAKY(0Z0afD<>Z`7H6C>S<ysd@=GIe#>JC4P4w$G
zf}|LP7&z=8W`Vg33=D_Bc8D+tpoyObD-dE}Koh?Q78hXPP(U^3BiI}<1_r2G!O9pI
z7}yyZ7=##jCvP_ql=NU^U{GKXXHY;>BR=_|iMXU7NF@^=gN6{Q$#RngO~oZ`L9z_I
z@SFn58z4K}COevnvj&4q2A2a#lM7A78S_DU7@H<9G!^%p2-Ud(8cwMoZ43+ydl?uQ
z1Q;Y3EYMuD5Tu@om!SX}C#+EQK9d>E#65R1LUh661S-jJ6r_uRmjO9Xg5*vyGB5}-
ziNoU%BnHB>CnuUoOg>}gz+z!wYPy-%d<v7jUP@|GX?lESURpi_l%1HARFql<<K<-L
zrNY?7B}Fi1ZelV>&*VfFkIgSE71$V~Cv!T;voeFS8z@jXyA42AGB7kv=CqP$<%f&&
z8bZV~!Q!%T@iM4*Hb`7i6C@5Qq#%mn<U^>cX0UB0AXQ-7Qj8!<7(u!xYdA=VW<W(e
q*dQ_rAk!v?I%sok0F_+~3=G#8CwDoRakYU8Lk0#0XU54~R&oFYF9_cN
diff --git a/examples/get_sign.bc b/examples/get_sign.bc
index 9b6d64807d3f7ca6e46b8102c0a0b438e2bc07a6..6b58850ce5098dcc54947def8b066de78515a9fe 100644
GIT binary patch
delta 1072
zcmdlZen4E+$@#!NQxOIRRt5%!Bpw45ugHCAvA?(Ya|br~FfuSODDp5c%$}&aon4HP
zfkFC^+Qi2tNyQV|3o_b^GMFnW+Di)9t2Edv84fkd-e6R?u~6n&qTDS8xhD%{jw#AM
zTPSnufXsu1vWFUF7>YUA%Vx9}F?5u9u$N~rmua+vL^7DGHQEaow3kn4H`~!(qQG9|
zz|O!o`77hH`l<=-RT}IKGuW#*+6yDv%^KJ%E7+^xss-As4A_e`*ef%dD?Qk2HP{*W
z8Jgq{Im(?|DDz?=?=eQXSBwYPZ8kKUZD6)y;HctYue4|{TF`E0&|bvBUbTX~Qlq_+
z;aY;s2S)xI3A|?*<)1mq-ALfQwNUm$Bk#2YdAVl`Wo{(!K1-B4<;Zs<f%gL=|2qbS
zR|jREDaxE#C^MOnNi?{lYDRleMssBadojpl_Ogohf(7gcWDYfgJm0|kQt8kC|Ns9x
z^c=Q6(QGs2u*C&t>nG0ACk|U*X||r=Y&pSMdV;gn4QHzf&X!va+8k-NxiEP>i&(uQ
z-%A7jhYEae0{C(r_#aN-dvk&9u>jwj1ALzuW;k1HIBYY8*<nVrO^dVj6lduJhpm@1
zTVHUtJi!cB!*G!AsR94z3v3@0_@5epjCy*3?HL3ATLHc&2<<x#TW@i++R<!z##wp>
zv&|Mq>lS9)1<VP24-ZT}z`|wlPJr*70e@}+--ioqZw2_iH1IW8wlG_takgY=vEJh>
zea6{pPP6qCX3H&&c2k;d_DoJ>k&$%Z|0KZofr0<!1HR`lZ49<2oNXsRVL3l}3#)#8
z0@u?EY;PB^KLt6Dy_|u)%7DFS0ei6mdoBZiQ2~1)m<<wyC{SRpN?<Qpz+UFSo;!iB
z%mK{3!1k<xy<h=*p#pow1-5q$>{SBnWe|-C>?If2HVd#9HL!c}a|ljyXzLN-WHfP-
z2s7+>Ib9%V@yAwKAqN)ci7X5ZEDQ_`jEp=hIa(MP6c`|&fkB}`QPf!iA`21|U|=y=
z(zJw?g8`HyKq5>H3@T<EBL74f7)~%TPHtgSV4S>pDVs8rp@H+mTi}HMfl=;MqRfj#
zw<|XfTeL7+Z#b-f!`bSLvsH())dpv)3(j^7l?n_DN|P^gsOn`ic(F4ulqY8-7R485
zR;7j}mFAU{DkSG5=A|o?r4|)u=I1FG8tNJ78R!}@Og7=PVU(O)$f;)`X7V_J?|A_K
zLk0dP4j}S*0N<Al4UM40U624uj)fec3|bUXFz2wv7DnqO&9+mR85kzd=X}ockws&{
w<Ss5bMz+Z-xs*9I7#J9Y85kI>Ctu~tW^|qG$gRe>dU6K08k3>n<bG})05A@9mH+?%
delta 1108
zcmX>gzDHcu$@#!NQxOIRRt5%!Bpw45&&Yjg?=Rcwx-c4ngcuZg7#L<vRNc;Q%E-VV
z9i~3<aY=odMtkLqcC!ZdN{#kHkM>H9b~6L^ij4LG1@;3nhZ<#{EtFwcBzx(g?5zgb
zQx8ERw+_giN|br=Q1;0}-gk<!CmQ80Fg7qZ6ttITFc(i~FUV*w%3!XjXfG*XuhL+z
z%xEr3XfMfNZ;*SkQ0^3?#GQw-w+_fWQIxs0Q05kcyxcuS**lGLryS*OEs(jPD0^!m
z@12LTcNX&ASSWMopv>f*jLYhaIoQi)v==dSR4!;QkZ3Q>V6K?ZUcR8cNP@kpg1s_>
zxo`!0u|a#$gm$wT?Ijo5ix@sID7;XVdGb)^RHNLj1epg5<rr!XFk5FZTQ6X4SkPWD
zp}kmxy()vbSfjmQL3`DN_M#c=3B1P`<v%p=UOOQ3AyMv0Bk#2ZvbPxJZzR<7K1-B4
z)yR7-LGIZ?nI{dr*BInKJm6zkBzGrK?$AM*Qww>|Fv{IpAbSWD6b9`D3GI~{><ufx
zfjOhS+yHD-LVGy}dlkbOMVT9ka;F$?7#JV=|NsAg{v#H9nr%)vTlO&9Zg95S(rB~C
z*>(rB<rHSiEsT~+nr)Xb*IQ0;mOkTbbAs7+OQYohXX!1@78jVU7@i66y)oc_${_G$
z0^er=zDEc6o?c-4BEa|Z0AH>F-@^kS*#^rNX6rM~mJBS`Qx4mlah5*NY%}Gs#gfA|
zQ=Fw|FxzZ#wwS=208;!pfREuJ-}?(}&lLC{UH}>O;RD~x2Yg=w>iIrhV0(Ii@8tzP
z2HO+Pwo{l5b{w|e(r9_Y*<y>c<rYSpJ<e7;m~E#t+iY>P+~91r#aVjCVe1{v(i@yD
zTbeByTCDdtOD}1*o^jX)y9eHV;LCl$_wWJV=L>Al82EE9@I7?kf59-r*<!<Cn<?VV
z4j}su+AKM2xx?9Vg0u7sXUh|ZttY==mXZ3R!2ghe|HA~ncLjW?`X*<xoS$sYYEU1*
z_VfbV+Xd`TFR;B#U@uv~Ugp4_o4{AWz+NT5Uev&z`+%=v0efKrdzAru5k%I2yHJ6>
zV!@XN0Y%P~6CM)<9F$uUMVn{TaT-d+-%w<9F%a=&U~phyU=R>EFrmwVgMopG0RlJ}
zm?VM>TNuHzAR#3NMh6CGEsv-M1_2PCfq_ARfx{uG*&)%Nk)c6HfPrDM1)Bn6=jKQ@
zWhPFLl1c>z2DQm+IaKXx7`mhx7|N3~5{u%CGpkaQa}x8?70ObJiZk=`6fE@&^bB;3
z6f{Z_(~I?kTzy;}gI(h-4Gi?tGV>C1G$(P|Fmg|}<<y(JnDaTy2NsP9ll!>j7+EK;
q<x=KUXJB9uW?*2jntYQho6%*mE4Lcss>wOrYK)eXr*P{qG5`Pz8kA@N
diff --git a/examples/get_sign.c b/examples/get_sign.c
index a10b519..d536444 100644
--- a/examples/get_sign.c
+++ b/examples/get_sign.c
@@ -177,13 +177,13 @@ int main()
// Did the result correspond to the expected path for the test?
//
// [your answer here]
-// Yes
-// echo $? gives 255 (which is equal to -1 of 8 signed bits)
+// No
+// echo $? gives 255
//
// Why not? Confer to shell error codes:
//
// [your answer here]
-// ??? TODO
+// In bash exit code 255 means "Exit status out of range" and it says "exit takes only integer args in the range 0 - 255". The result should have been -1 but it is out of range for bash, so that is why I didn't get the expected result.
//
// D) Debugging
//
diff --git a/examples/klee-last b/examples/klee-last
index c01e645..fd456c4 120000
--- a/examples/klee-last
+++ b/examples/klee-last
@@ -1 +1 @@
-/home/niklas/Desktop/D7020E/klee_tutorial/examples/klee-out-0
\ No newline at end of file
+/home/niklas/Desktop/D7020E/klee_tutorial/examples/klee-out-1
\ No newline at end of file
diff --git a/examples/klee-out-1/assembly.ll b/examples/klee-out-1/assembly.ll
new file mode 100644
index 0000000..a9095db
--- /dev/null
+++ b/examples/klee-out-1/assembly.ll
@@ -0,0 +1,60 @@
+; ModuleID = 'get_sign.bc'
+source_filename = "get_sign.c"
+target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-pc-linux-gnu"
+
+@.str = private unnamed_addr constant [2 x i8] c"a\00", align 1
+
+; Function Attrs: noinline nounwind optnone uwtable
+define dso_local i32 @get_sign(i32 %0) #0 {
+ %2 = alloca i32, align 4
+ %3 = alloca i32, align 4
+ store i32 %0, i32* %3, align 4
+ %4 = load i32, i32* %3, align 4
+ %5 = icmp eq i32 %4, 0
+ br i1 %5, label %6, label %7
+
+6: ; preds = %1
+ store i32 0, i32* %2, align 4
+ br label %12
+
+7: ; preds = %1
+ %8 = load i32, i32* %3, align 4
+ %9 = icmp slt i32 %8, 0
+ br i1 %9, label %10, label %11
+
+10: ; preds = %7
+ store i32 -1, i32* %2, align 4
+ br label %12
+
+11: ; preds = %7
+ store i32 1, i32* %2, align 4
+ br label %12
+
+12: ; preds = %11, %10, %6
+ %13 = load i32, i32* %2, align 4
+ ret i32 %13
+}
+
+; Function Attrs: noinline nounwind optnone uwtable
+define dso_local i32 @main() #0 {
+ %1 = alloca i32, align 4
+ %2 = alloca i32, align 4
+ store i32 0, i32* %1, align 4
+ %3 = bitcast i32* %2 to i8*
+ call void @klee_make_symbolic(i8* %3, i64 4, i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str, i64 0, i64 0))
+ %4 = load i32, i32* %2, align 4
+ %5 = call i32 @get_sign(i32 %4)
+ ret i32 %5
+}
+
+declare dso_local void @klee_make_symbolic(i8*, i64, i8*) #1
+
+attributes #0 = { noinline nounwind optnone uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
+attributes #1 = { "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
+
+!llvm.module.flags = !{!0}
+!llvm.ident = !{!1}
+
+!0 = !{i32 1, !"wchar_size", i32 4}
+!1 = !{!"Ubuntu clang version 11.0.0-2"}
diff --git a/examples/klee-out-1/info b/examples/klee-out-1/info
new file mode 100644
index 0000000..1f816e9
--- /dev/null
+++ b/examples/klee-out-1/info
@@ -0,0 +1,22 @@
+klee get_sign.bc
+PID: 232064
+Using monotonic steady clock with 1/1000000000s resolution
+Started: 2020-12-15 16:48:54
+BEGIN searcher description
+<InterleavedSearcher> containing 2 searchers:
+RandomPathSearcher
+WeightedRandomSearcher::CoveringNew
+</InterleavedSearcher>
+END searcher description
+Finished: 2020-12-15 16:48:54
+Elapsed: 00:00:00
+KLEE: done: explored paths = 3
+KLEE: done: avg. constructs per query = 11
+KLEE: done: total queries = 3
+KLEE: done: valid queries = 0
+KLEE: done: invalid queries = 3
+KLEE: done: query cex = 3
+
+KLEE: done: total instructions = 31
+KLEE: done: completed paths = 3
+KLEE: done: generated tests = 3
diff --git a/examples/klee-out-1/messages.txt b/examples/klee-out-1/messages.txt
new file mode 100644
index 0000000..d49ad73
--- /dev/null
+++ b/examples/klee-out-1/messages.txt
@@ -0,0 +1 @@
+KLEE: Using Z3 solver backend
diff --git a/examples/klee-out-1/run.istats b/examples/klee-out-1/run.istats
new file mode 100644
index 0000000..9631323
--- /dev/null
+++ b/examples/klee-out-1/run.istats
@@ -0,0 +1,52 @@
+version: 1
+creator: klee
+pid: 232064
+cmd: get_sign.bc
+
+
+positions: instr line
+event: Icov : CoveredInstructions
+event: Forks : Forks
+event: Ireal : InstructionRealTimes
+event: Itime : InstructionTimes
+event: I : Instructions
+event: UCdist : MinDistToUncovered
+event: Rtime : ResolveTime
+event: States : States
+event: Iuncov : UncoveredInstructions
+event: Q : Queries
+event: Qiv : QueriesInvalid
+event: Qv : QueriesValid
+event: Qtime : QueryTime
+events: Icov Forks Ireal Itime I UCdist Rtime States Iuncov Q Qiv Qv Qtime
+ob=assembly.ll
+fn=get_sign
+10 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+11 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+12 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+13 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+14 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+15 0 1 1 0 0 1 0 0 0 0 2 2 0 32370
+18 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+19 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+22 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+23 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+24 0 1 1 0 0 1 0 0 0 0 1 1 0 13814
+27 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+28 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+31 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+32 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+35 0 1 0 0 0 3 0 0 0 0 0 0 0 0
+36 0 1 0 0 0 3 0 0 0 0 0 0 0 0
+fn=main
+41 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+42 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+43 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+44 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+45 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+46 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+47 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+cfn=get_sign
+calls=1 8 0
+47 0 17 2 0 0 21 0 0 0 0 3 3 0 46184
+48 0 1 0 0 0 3 0 0 0 0 0 0 0 0
diff --git a/examples/klee-out-1/run.stats b/examples/klee-out-1/run.stats
new file mode 100644
index 0000000000000000000000000000000000000000..160d68a57724c30a1c336cc780df730dca12c7bf
GIT binary patch
literal 8192
zcmWFz^vNtqRY=P(%1ta$FlG>7U}9o$P*7lCU|@n`1}I=;U|?W@vOyGx52Ep5CI&tC
z6}$`#42*p041DVNl#a@chQMeDjE2By2#kinXb6mkz-S1JhQMeDjE2By2n>P{Xbxj!
z7Z(?2Z09aXOv*_uE=epY1`|xqL9UJ=t_mTJPCl**U?Bw!&%EN2qSEA&%>2A!1y8>a
zS9jMS9k<e)9H*khyyT2jgkV5oQAuVZrnp~eE{59B;?$y$%-mFkAXi5p9lz4t;F81=
zB(r=Ib8_;NLyHsBQ{k5SmF5PPrWR!)DT4}CI_E=OiEvGLVonai2Iu^;)S}cBtey$Y
zOU5G$va%9v5X|$z`8j1!*TaOIQ!AVklQU9L)VbvsWupiLr51y<qKJWwhiUiCEG|a!
z9g3VsW(mS`jzvX@l^%)38OUa7g8Jr6{A(Ea@AI!21nF$l38Nt}8UmvsFd71*Aut*O
zqaiRF0;3@?8UmvsFd71*Au!@Yz>rClk&%OunS+^;k(rT$nVFf9gOQO@o{5R!$$FvX
zCzur(_Dz&z*pk7pRf=KDE*WN)|MHBY92^{sOdQM{984UH91y_Bq^mDj_<=1%@;?BR
CtGFQm
literal 0
HcmV?d00001
diff --git a/examples/klee-out-1/test000001.ktest b/examples/klee-out-1/test000001.ktest
new file mode 100644
index 0000000000000000000000000000000000000000..25f74a85d90a98ba12009cab156dd058ea9079b6
GIT binary patch
literal 53
vcmeYcaSaY(U|?WoU|?WmU|`@*Pc4Zr&P>nKOG;)y0FV@8A_D^h3rGwA*{%jf
literal 0
HcmV?d00001
diff --git a/examples/klee-out-1/test000002.ktest b/examples/klee-out-1/test000002.ktest
new file mode 100644
index 0000000000000000000000000000000000000000..052994a96ef7578d3e66bc8ba1bd04b3fb521309
GIT binary patch
literal 53
xcmeYcaSaY(U|?WoU|?WmU|`@*Pc4Zr&P>nKOG;)y0FV@8A_D^h%YOz21_0fv2Sfk>
literal 0
HcmV?d00001
diff --git a/examples/klee-out-1/test000003.ktest b/examples/klee-out-1/test000003.ktest
new file mode 100644
index 0000000000000000000000000000000000000000..181f91f22038d0ca19e866aad982d22d6ba68a44
GIT binary patch
literal 53
xcmeYcaSaY(U|?WoU|?WmU|`@*Pc4Zr&P>nKOG;)y0FV@8A_D^h3j+f~0|44C2E_mX
literal 0
HcmV?d00001
diff --git a/examples/klee-out-1/warnings.txt b/examples/klee-out-1/warnings.txt
new file mode 100644
index 0000000..e69de29
--
GitLab