Using assertions

[Alexandru Copot]

Hi,

I managed to build the stable branch of UFO and run the tests. All the 7 tests pass. I also built the

UFO Front End. However, I don't know if it actually detects violations. For example, both the correct

and buggy bubble-sort show as having errors. When I run the source code with ufo.py, both show up

as not having errors. Can anyone provide the simplest pair of correct and with-bugs example of

using assertions ?

Thanks!  

[Arie Gurfinkel]

Hey Alexandru, 

please use develop or master branch. stable branch is old and is not maintained.

This thread provides extra instructions on how to compile new version 

https://groups.google.com/forum/#!topic/ufo-discuss/xdTDiqdvAJY

If you are planning to use self-compiled binary with ufo front-end, remove --ufo-abc-simplify=true from the front-end, unless you compiled ufo with the optional abc library.

You can find many simple examples in the sv-comp repo. For example, 

https://svn.sosy-lab.org/software/sv-benchmarks/tags/svcomp14/ssh-simplified/s3_clnt_1_false.cil.c

https://svn.sosy-lab.org/software/sv-benchmarks/tags/svcomp14/ssh-simplified/s3_clnt_1_true.cil.c

cheers,

arie

--
You received this message because you are subscribed to the Google Groups "UFO General Discussion Group" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ufo-discuss...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Alexandru Copot]

On Sunday, 1 March 2015 15:47:47 UTC+1, Arie Gurfinkel wrote:

Hey Alexandru, 

please use develop or master branch. stable branch is old and is not maintained.

This thread provides extra instructions on how to compile new version 

https://groups.google.com/forum/#!topic/ufo-discuss/xdTDiqdvAJY

If you are planning to use self-compiled binary with ufo front-end, remove --ufo-abc-simplify=true from the front-end, unless you compiled ufo with the optional abc library.

You can find many simple examples in the sv-comp repo. For example, 

https://svn.sosy-lab.org/software/sv-benchmarks/tags/svcomp14/ssh-simplified/s3_clnt_1_false.cil.c

https://svn.sosy-lab.org/software/sv-benchmarks/tags/svcomp14/ssh-simplified/s3_clnt_1_true.cil.c

I've rebuild UFO from master with Z3 from unstable. I've compared its output with the one from the binary you

used on SVCOMP2013. My build cannot find assertion violations and never prints counter-examples. So now

I am certain the examples are good, just the ufo built from source has some issues. Any way I could debug this ?

 

Thanks!

Alex

[Arie Gurfinkel]

Send me your command line, output, and inputs you are using. 

cheers

arie

--
On the move ...

[Alexandru Copot]

I am running it like this:

./ufo-svcomp-par.py array_safe.c

./ufo-svcomp-par.py --cex=cex_file array_unsafe.c

The inputs:

https://svn.sosy-lab.org/software/sv-benchmarks/tags/svcomp13/loops/array_safe.c

https://svn.sosy-lab.org/software/sv-benchmarks/tags/svcomp13/loops/array_unsafe.c

The outputs are attached. The build was made with the script from the other thread.

If I just replace the ufo binary with the one from SVCOMP, everything works fine.

To unsubscribe from this group and stop receiving emails from it, send an email to ufo-discuss+unsubscribe@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

[Arie Gurfinkel]

Hey, the output says that the problem is solved by the front-end. Namely, it removes all error location from main() before ufo has a chance to run. I'm not sure how changing ufo binaries would change this. This example is problematic in general because it uses dynamically sized stack allocated arrays that are not well supported. You are also using examples from SV-COMP'13 have slightly different conventions than SV-COMP'14. 

Please send me the files generated by the front-end:

  mkdir tmp

  ./ufo-svcomp-par.py --save-temps --temp-dir=tmp FILE.c

then zip and send me the tmp directory. I'll double check whether it is the front-end or ufo that are causing this.

cheers,

arie

[Alexandru Copot]

Hi,

I attached the temp directory. Thanks for all the help.

Alex

>>> On the move ...
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "UFO General Discussion Group" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to ufo-discuss...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>
>

[Arie Gurfinkel]

Hey Alexandru,

are you using binaries from svcomp 13 or 14 as the starting point?

Please use the SVCOMP14 distribution from here: 

              https://bitbucket.org/arieg/ufo/wiki/svcomp14

cheers,

arie