Hi Christian,
If I recall correctly, 'seq' at some points uses a long double to
represent the size. I think what is happening in this case is that a
double is getting extended to a (x86) long double, and that code was
never written.
There should be code in llvm's APFloat.h which can be used to
implement this. (Or if you don't care about long double, you could
just hack the code to not assert).
- Daniel
On Fri, Sep 25, 2009 at 2:23 PM, Cristian Zamfir
<cristian.zamfir at epfl.ch> wrote:
>
>
> Hi,
>
> I am trying to use a previous version of klee on "seq".
> I am running with these parameters:
>
> klee --simplify-sym-indices --max-sym-array-size 4096 --write-cvcs --
> write-cov --output-module --max-memory=3000 --disable-inlining --use-
> forked-stp --use-cex-cache --with-libc --with-file-model=release --
> allow-external-sym-calls --exclude-libc-cov --optimize --only-output-
> states-covering-new --run-in=/home/zamf/sandbox ?--max-instruction-
> time=10. --max-time=3600. --watchdog --max-memory-inhibit=false --max-
> static-fork-pct=1 --max-static-solve-pct=1 --max-static-cpfork-pct=1 --
> switch-type=internal --randomize-fork --use-random-path --use-
> interleaved-covnew-NURS --use-batching-search --batch-instructions
> 10000 --init-env ./seq.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-
> files 1 8 --sym-stdout
>
> and I get this error
>
> DEMAND FAILED:util/FloatEvaluation.h:ext:193: <inWidth==32> is false:
> "can only extend from a 32-bit float"
>
> The error comes from the first demand in this function which is called
> with inWidth = 64.
>
> // extension of l (which must be a float) to double (casts a float to
> a double)
> inline uint64_t ext(uint64_t l, unsigned outWidth, unsigned inWidth) {
> ? klee_warning("inwidth = %d", inWidth);
> ? demand( ?inWidth==32, "can only extend from a 32-bit float" );
> ? demand( outWidth==64, "can only extend to a 64-bit double" ?);
> ? double ext = (double)UInt64AsFloat(l);
> ? return bits64::truncateToNBits(DoubleAsUInt64(ext), outWidth);
> }
> from lib/util/FloatEvaluation.h
>
> Did you run into this error before?
>
> Thank you,
> Cristi
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
