[prev in list] [next in list] [prev in thread] [next in thread]
List: klee-dev
Subject: Re: [klee-dev] About filename extension of symbolic files
From: Weiqi Wang <wq.wang () mail ! utoronto ! ca>
Date: 2021-08-22 23:54:39
Message-ID: YQXPR0101MB0855E83208DA157942D51502C0C39 () YQXPR0101MB0855 ! CANPRD01 ! PROD ! OUTLOOK ! COM
[Download RAW message or body]
Hi,
I’m posting my solution here in case anybody else would find it useful.
Commenting out https://github.com/klee/klee/blob/master/runtime/POSIX/fd.c#L60-L61 \
works in my case. If anyone would like to use the same approach, keep in mind that \
any filename starting with A, B … would now be symbolic.
Best,
Weiqi
From: Weiqi Wang<mailto:wq.wang@mail.utoronto.ca>
Sent: Friday, August 20, 2021 6:55 PM
To: klee-dev@imperial.ac.uk<mailto:klee-dev@imperial.ac.uk>
Subject: [klee-dev] About filename extension of symbolic files
EXTERNAL EMAIL:
Hi,
I was trying to run klee with GraphicsMagick(GM) using command:
klee --disable-verify --only-replay-seeds --libc=uclibc --posix-runtime --seed-file \
rectangular.ktest ./gm.bc identify A -sym-files 1 80
rectangular.ktest is generated using `gen-bout –sym-file rectangular.mvg –but-file \
rectangular.ktest` Content of rectangular.mvg:
push graphic-context
viewbox 0 0 100 60
rectangle 5,5 15,15
pop graphic-context
In the output I saw GM complains:
./gm.bc identify: No decode delegate for this image format (A)
./gm.bc identify: Request did not return an image
I suspect this is because GM checks the filename extension. Because when I run it \
without klee `gm identify A` returns same error
`gm identify A.mvg` works fine
(In this case I manually created concrete file A and A.mvg containing the same \
content as rectangular.mvg)
Could anyone explain how to specify symbolic file with extensions?
Best,
Weiqi
[Attachment #3 (text/html)]
<html xmlns:o="urn:schemas-microsoft-com:office:office" \
xmlns:w="urn:schemas-microsoft-com:office:word" \
xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" \
xmlns="http://www.w3.org/TR/REC-html40"> <head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:DengXian;
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:"\@DengXian";
panose-1:2 1 6 0 3 1 1 1 1 1;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
span.DefaultFontHxMailStyle
{mso-style-name:"Default Font HxMail Style";
font-family:"Arial",sans-serif;
color:windowtext;
font-weight:normal;
font-style:normal;
text-decoration:none none;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri",sans-serif;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.25in 1.0in 1.25in;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-US" link="blue" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><span class="DefaultFontHxMailStyle">Hi,<o:p></o:p></span></p>
<p class="MsoNormal"><span \
class="DefaultFontHxMailStyle"><o:p> </o:p></span></p> <p \
class="MsoNormal"><span class="DefaultFontHxMailStyle">I’m posting my solution here \
in case anybody else would find it useful.<o:p></o:p></span></p> <p \
class="MsoNormal"><span class="DefaultFontHxMailStyle">Commenting out <a \
href="https://github.com/klee/klee/blob/master/runtime/POSIX/fd.c#L60-L61"> \
https://github.com/klee/klee/blob/master/runtime/POSIX/fd.c#L60-L61</a> works in my \
case. <o:p></o:p></span></p>
<p class="MsoNormal"><span class="DefaultFontHxMailStyle">If anyone would like to use \
the same approach, keep in mind that any filename starting with A, B … would now be \
symbolic.<o:p></o:p></span></p> <p class="MsoNormal"><span \
class="DefaultFontHxMailStyle"><o:p> </o:p></span></p> <p \
class="MsoNormal"><span class="DefaultFontHxMailStyle">Best,<o:p></o:p></span></p> <p \
class="MsoNormal"><span class="DefaultFontHxMailStyle">Weiqi<o:p></o:p></span></p> <p \
class="MsoNormal"><span class="DefaultFontHxMailStyle"><o:p> </o:p></span></p> \
<div style="mso-element:para-border-div;border:none;border-top:solid #E1E1E1 \
1.0pt;padding:3.0pt 0in 0in 0in"> <p class="MsoNormal" \
style="border:none;padding:0in"><b>From: </b><a \
href="mailto:wq.wang@mail.utoronto.ca">Weiqi Wang</a><br> <b>Sent: </b>Friday, August \
20, 2021 6:55 PM<br> <b>To: </b><a \
href="mailto:klee-dev@imperial.ac.uk">klee-dev@imperial.ac.uk</a><br> <b>Subject: \
</b>[klee-dev] About filename extension of symbolic files</p> </div>
<p class="MsoNormal"><span \
class="DefaultFontHxMailStyle"><o:p> </o:p></span></p> <div>
<p class="MsoNormal"><strong><span \
style="font-size:10.0pt;font-family:"Arial",sans-serif;color:#C75000">EXTERNAL \
EMAIL:</span></strong><b><span \
style="font-size:10.0pt;color:white"><o:p></o:p></span></b></p> </div>
<div>
<p class="MsoNormal"><span class="DefaultFontHxMailStyle">Hi,<o:p></o:p></span></p>
<p class="MsoNormal"><span \
class="DefaultFontHxMailStyle"><o:p> </o:p></span></p> <p \
class="MsoNormal"><span class="DefaultFontHxMailStyle">I was trying to run klee with \
GraphicsMagick(GM) using command: <o:p></o:p></span></p>
<p class="MsoNormal"><span \
class="DefaultFontHxMailStyle"><o:p> </o:p></span></p> <p \
class="MsoNormal"><span class="DefaultFontHxMailStyle">klee --disable-verify \
--only-replay-seeds --libc=uclibc --posix-runtime --seed-file rectangular.ktest \
./gm.bc identify A -sym-files 1 80<o:p></o:p></span></p> <p class="MsoNormal"><span \
class="DefaultFontHxMailStyle"><o:p> </o:p></span></p> <p \
class="MsoNormal"><span class="DefaultFontHxMailStyle">rectangular.ktest is generated \
using `gen-bout –sym-file rectangular.mvg –but-file rectangular.ktest` \
<o:p></o:p></span></p> <p class="MsoNormal"><span \
class="DefaultFontHxMailStyle">Content of rectangular.mvg:<o:p></o:p></span></p> <p \
class="MsoNormal"><span \
class="DefaultFontHxMailStyle"> \
push graphic-context<o:p></o:p></span></p> <p class="MsoNormal" \
style="text-indent:.5in"><span class="DefaultFontHxMailStyle">viewbox 0 0 100 \
60<o:p></o:p></span></p> <p class="MsoNormal" style="text-indent:.5in"><span \
class="DefaultFontHxMailStyle">rectangle 5,5 15,15<o:p></o:p></span></p> <p \
class="MsoNormal" style="text-indent:.5in"><span class="DefaultFontHxMailStyle">pop \
graphic-context<o:p></o:p></span></p> <p class="MsoNormal"><span \
class="DefaultFontHxMailStyle"><o:p> </o:p></span></p> <p \
class="MsoNormal"><span class="DefaultFontHxMailStyle">In the output I saw GM \
complains:<o:p></o:p></span></p> <p class="MsoNormal"><span \
class="DefaultFontHxMailStyle"><o:p> </o:p></span></p> <p \
class="MsoNormal"><span class="DefaultFontHxMailStyle">./gm.bc identify: No decode \
delegate for this image format (A)<o:p></o:p></span></p> <p class="MsoNormal"><span \
class="DefaultFontHxMailStyle">./gm.bc identify: Request did not return an \
image<o:p></o:p></span></p> <p class="MsoNormal"><span \
class="DefaultFontHxMailStyle"><o:p> </o:p></span></p> <p \
class="MsoNormal"><span class="DefaultFontHxMailStyle">I suspect this is because GM \
checks the filename extension. Because when I run it without \
klee<o:p></o:p></span></p> <p class="MsoNormal"><span \
class="DefaultFontHxMailStyle">`gm identify A` returns same \
error<o:p></o:p></span></p> <p class="MsoNormal"><span \
class="DefaultFontHxMailStyle">`gm identify A.mvg` works fine<o:p></o:p></span></p> \
<p class="MsoNormal"><span class="DefaultFontHxMailStyle">(In this case I manually \
created concrete file A and A.mvg containing the same content as \
rectangular.mvg)<o:p></o:p></span></p> <p class="MsoNormal"><span \
class="DefaultFontHxMailStyle"><o:p> </o:p></span></p> <p \
class="MsoNormal"><span class="DefaultFontHxMailStyle">Could anyone explain how to \
specify symbolic file with extensions?<o:p></o:p></span></p> <p \
class="MsoNormal"><span class="DefaultFontHxMailStyle"><o:p> </o:p></span></p> \
<p class="MsoNormal"><span class="DefaultFontHxMailStyle">Best,<o:p></o:p></span></p> \
<p class="MsoNormal"><span class="DefaultFontHxMailStyle">Weiqi<o:p></o:p></span></p> \
</div> <p class="MsoNormal"><span \
class="DefaultFontHxMailStyle"><o:p> </o:p></span></p> <p \
class="MsoNormal"><span class="DefaultFontHxMailStyle"><o:p> </o:p></span></p> \
</div> </body>
</html>
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
--===============1504975734523576481==--
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic