Re: [klee-dev] a question about kleaver

[Dan Liew]

Hi,

On 8 January 2016 at 10:18, xiaoqixue_1  wrote:
>
>
> Hi,
>
> When a use kleaver to solve a query, I found that "Ult" and "Ugt" can not be 
> used at the same time.
> the logic is simple:
> if( sn > 5) {
>if( sn < 8 ) {
>  if (sn==0) printf("hello");
>  }
> }
>
> the query is as follows:
>  
>array sn[4] : w32 -> w8 = symbolic
>  (query [(Ult 5
>  N0:(ReadLSB w8 0 sn))
> (Ugt N0 8) ]
>   (Eq N0 0) [] [ sn ] )
>  
>
> it  crashes the kleaver, but when I change the file to :

The crash is due to Ult not being supported by the STPBuilder. In KLEE
a Ult expression shouldn't ever occur due to expression
canonicalisation rules used internally inside KLEE. The assertion
failure you hit is

Query 0:kleaver:
/home/dan/dev/klee/src/lib/Solver/STPBuilder.cpp:903: klee::ExprHandle
klee::STPBuilder::constructActual(klee::ref, int*):
Assertion `0 && "unhandled Expr type"' failed.

Take a look at ``include/klee/Expr.h`` to get an explanation of why
these rules exists. If you pass `` --builder=simplify`` to kleaver the
expression builder should try to canonicalise the expressions for you
and avoid the crash.

Hope that helps.
Dan.

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

[klee-dev] a question about kleaver

[xiaoqixue_1]

Hi,

When a use kleaver to solve a query, I found that "Ult" and "Ugt" can not be 
used at the same time.
the logic is simple:
if( sn > 5) {
       if( sn < 8 ) {
 if (sn==0) printf("hello");
 }
}

the query is as follows:
 
   array sn[4] : w32 -> w8 = symbolic   

  
 (query [(Ult 5 

    
 N0:(ReadLSB w8 0 sn))  

 
    (Ugt N0 8) ]

  
  (Eq N0 0) [] [ sn ] ) 
 

it  crashes the kleaver, but when I change the file to :

   array sn[4] : w32 -> w8 = symbolic   

  
 (query [(Ult 5 


 N0:(ReadLSB w8 0 sn))  

 
(Ult N0 8) ]

  
  (Eq N0 0) [] [ sn ] ) 
=

it  works normal.

could you tell me why ?
What is different between "Ugt" and "Ult", or I have made some mistake when 
using kleaver?

Thanks.

Good Luck!




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