[klee-dev] Compiling KLEE - metaSMT support

Cristian Cadar c.cadar at imperial.ac.uk
Wed Dec 3 09:33:17 GMT 2014


Hi Thuan,

I moved the repository from /ccadar to /klee/ (The /ccadar URL simply
redirects to the /klee one now.)  I will fix the webpage, thanks for
pointing out the inconsistency.

Cristian

On 03/12/2014 02:14, Thuan Pham wrote:
> Hello Hristina,
> Thank you very much, it works now.
> I have one more question. According to the tutorials for compiling the
> vanilla KLEE and KLEE-metaSMT, it seems that there are two "mainline"
> KLEE repositories at 
> https://github.com/klee/klee.git
> https://github.com/ccadar/klee.git
> Are they synchronized or separately maintained? 
> I ask the question because I plan to build something on top of
> KLEE-metaSMT and I want to keep my system compatible with the newest
> vanilla KLEE.
> Thuan.
> 
> On Wed, Dec 3, 2014 at 3:06 AM, Hristina Palikareva
> <h.palikareva at imperial.ac.uk <mailto:h.palikareva at imperial.ac.uk>> wrote:
> 
>     Hello Thuan,
> 
>     There was a small regression error which has now been fixed. Please try
>     with the newest version of KLEE and let me know if you have any
>     problems.
> 
>     Thank you very much for pointing this out!
> 
>     Best wishes,
>     Hristina
> 
> 
> 
>     On 01/12/14 06:55, Thuan Pham wrote:
>     > FYI, I have compiled successfully the vanilla KLEE on my machine. I am
>     > using Ubuntu 12.04 64-bit.
>     > Thanks.
>     >
>     > On Mon, Dec 1, 2014 at 2:51 PM, Thuan Pham <thuanpv at comp.nus.edu.sg <mailto:thuanpv at comp.nus.edu.sg>
>     > <mailto:thuanpv at comp.nus.edu.sg <mailto:thuanpv at comp.nus.edu.sg>>> wrote:
>     >
>     >     Hello Hristina,
>     >     The file unordered_map.hpp is already there,
>     >     at /home/thuan/KLEE/metaSMT/deps/boost-1_52_0/include/boost/tr1
>     >
>     >     I have set the CPATH to point to your suggested path but it still
>     >     doesn't work.
>     >     Thanks,
>     >     Thuan.
>     >
>     >     On Sat, Nov 29, 2014 at 3:18 AM, Hristina Palikareva
>     >     <h.palikareva at imperial.ac.uk
>     <mailto:h.palikareva at imperial.ac.uk>
>     <mailto:h.palikareva at imperial.ac.uk
>     <mailto:h.palikareva at imperial.ac.uk>>>
>     >     wrote:
>     >
>     >         Hello Thuan,
>     >
>     >         Would you confirm that you have unordered_map.hpp under
>     >
>     >         /home/thuan/KLEE/metaSMT/deps/boost-1_52_0/include/boost/tr1?
>     >
>     >         If so, you need to set CPATH to point to
>     >         /home/thuan/KLEE/metaSMT/deps/boost-1_52_0/include. Also
>     note the
>     >         spelling of "CPLUS_INCLUDE_PATH".
>     >
>     >         Please let me know whether that works.
>     >
>     >         Best wishes,
>     >         Hristina
>     >
>     >
>     >
>     >         > Hello,
>     >         > I followed the instructions
>     >         > at
>     >       
>      http://srg.doc.ic.ac.uk/projects/klee-multisolver/getting-started.html
>     >         to
>     >         > compile KLEE-metaSMT.
>     >         > I did compile metaSMT successfully but I faced error while
>     >         configure and
>     >         > compile KLEE with metaSMT. Here is the output error:
>     >         >
>     >       
>      /home/thuan/KLEE/metaSMT/deps/boost-1_52_0/include/boost/tr1/unordered_map.hpp:16:66:
>     >         > fatal error: ../4.6.3/tr1/std::tr1::unordered_map: No such
>     >         file or directory
>     >         > compilation terminated.
>     >         >
>     >         > The name of the missing file looks strange. And here is the
>     >         indicated
>     >         > source of the error:
>     >         > include BOOST_TR1_STD_HEADER(BOOST_TR1_PATH(unordered_map))
>     >         >
>     >         > I have tried to update environment variables like
>     C_INCLUDE_PATH,
>     >         > CPUS_INCLUDE_PATH for boost library but it doesn't work.
>     >         > Could you please give me some suggestions to fix the issue.
>     >         > Thanks
>     >         >
>     >         >
>     >         >
>     >         > _______________________________________________
>     >         > klee-dev mailing list
>     >         > klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>     <mailto:klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>>
>     >         > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>     >         >
>     >
>     >
>     >         _______________________________________________
>     >         klee-dev mailing list
>     >         klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>     <mailto:klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>>
>     >         https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>     >
>     >
>     >
> 
> 
>     _______________________________________________
>     klee-dev mailing list
>     klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>     https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> 
> 
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> 



More information about the klee-dev mailing list