[ldv-project] Benchmarking new predicate analysis with UFs

[Philipp Wendler]

Hi,

Am 27.08.2013 13:31, schrieb Mikhail Mandrykin:
> No, so I've re-run the benchmark with this option. But it seems it won't
> influence the results greatly, because when I manually re-run the failed
> benchmarks with the option (used options attached in
> UsedConfiguration.properties), at least 9 out of 12 failures persisted. The
> exceptions are basically typing errors like these ones:
>
> 6x 			java.lang.IllegalArgumentException: A symbol with name `action at 4'
> already exists, with type: <BitVec, 64, >
> 2x			 java.lang.IllegalArgumentException: bv extraction of an empty range:
> [22671:22672]
> 1x			type error. term eeprom_wait_ready::status at 3 has type <BitVec, 64, >,
> but <BitVec, 48, > was expected. (make_equal)

Yes, there were a few exceptions with bitprecise analysis left.
I have implemented several fixes for them in the last few days and they 
should be all gone now.
I also make pointer alias handling more precise in several cases.
So if you are interested in current results, you could rerun the benchmarks.

Greetings, Philipp
-- 
Philipp Wendler
Lehrstuhl für Softwaresysteme
Universität Passau
Raum IM 110 - Tel.: 0851/509-3093