Re: [klee-dev] measuring the coverage using the test cases testN.TYPE.err

2017-08-07 Thread Andrew Santosa
Hi BNM,
If I understand correctly, here there are two categories of test suites 
discussed: one contains the test suite generatedby KLEE, and another contains 
test suites that come with the program itself. If you want to measure the 
coveragespecifically achieved by KLEE, then you should only run your program 
with the KLEE-generated test suite.

Andrew
On Sunday, August 6, 2017, 11:47:35 AM GMT+8, BNM  wrote:

 Hello,
I've tried to measure the code coverage of a program using Gcov with the test 
cases generated by KLEE . The test suites include some test cases reporting 
some errors, is it necessary to include these test cases when I measure the 
coverage or should be excluded?
Thank you,___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


Re: [klee-dev] SSE Support?

2017-08-07 Thread Owl Owl
Yeah I spent a few hours last night trying to compile libc with that flag.
It doesn't seem possible since functions like atof necessarily have to use
SSE for the return value.

On Aug 7, 2017 12:15, "David Lightstone" 
wrote:

> With respect to a SSE disabled version of QEMU
>
>
> The gcc compiler has options of the form -no-sse*
> My uninformed guess (i.e. I have not tried it) is the use of those options
> would be the key.
>
> You probably will have to build your own versions of libc and QEMU using
> those options
>
> Dave Lightstone
>
> Sent from my iPad
>
> > On Aug 7, 2017, at 4:00 AM, Owl Owl  wrote:
> >
> > Folks,
> >
> > Is there symbolic support for SSE regs? The amd64 ABI specifies that SSE
> must be present on those architectures, and i have not been successful in
> convincing libc to NOT use SSE enabled versions of it's functions.
> >
> > Looking for information on either KLEE support for this, or how to force
> an application in QEMU into using non-SSE libc functions.
> >
> > Aside: Given how things are evolving, it would appear that SSE will
> simply grow more prevalent and harder to avoid...
> >
> > Best,
> >
> > Mike
> > ___
> > klee-dev mailing list
> > klee-dev@imperial.ac.uk
> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


Re: [klee-dev] SSE Support?

2017-08-07 Thread David Lightstone
With respect to a SSE disabled version of QEMU


The gcc compiler has options of the form -no-sse*
My uninformed guess (i.e. I have not tried it) is the use of those options 
would be the key.

You probably will have to build your own versions of libc and QEMU using those 
options

Dave Lightstone

Sent from my iPad

> On Aug 7, 2017, at 4:00 AM, Owl Owl  wrote:
> 
> Folks,
> 
> Is there symbolic support for SSE regs? The amd64 ABI specifies that SSE must 
> be present on those architectures, and i have not been successful in 
> convincing libc to NOT use SSE enabled versions of it's functions.
> 
> Looking for information on either KLEE support for this, or how to force an 
> application in QEMU into using non-SSE libc functions.
> 
> Aside: Given how things are evolving, it would appear that SSE will simply 
> grow more prevalent and harder to avoid...
> 
> Best,
> 
> Mike
> ___
> klee-dev mailing list
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


[klee-dev] SSE Support?

2017-08-07 Thread Owl Owl
Folks,

Is there symbolic support for SSE regs? The amd64 ABI specifies that SSE
must be present on those architectures, and i have not been successful in
convincing libc to NOT use SSE enabled versions of it's functions.

Looking for information on either KLEE support for this, or how to force an
application in QEMU into using non-SSE libc functions.

Aside: Given how things are evolving, it would appear that SSE will simply
grow more prevalent and harder to avoid...

Best,

Mike
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev