about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2009-06-04Added a couple of tests for ReadLSB/MSB. Changed kleaver to write to stdout.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72841 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Fixed the code dealing with ReadLSB/ReadMSB, which was currentlyCristian Cadar
broken (it was written for n-ary Concats, but now we have binary Concats.) git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72840 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Implement simplify_type for ref<>Daniel Dunbar
- This allows dyn_cast<> and friends to be applied to a ref. For example, if (ConstantExpr *CE = dyn_cast<ConstantExpr>(foo)) { ... do something with CE ... } - This makes working with ref<Expr>s much more convenient, with the downside that it hides a potentially dangerous operation. Since the result is not itself a ref<>; clients are resposible for making sure the returned value is only used inside the lifetime of some other ref<>. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72839 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04TimingSolver shouldn't need a vtable.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72833 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Expr: Add LLVM style casting support instead of requiring RTTI.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72829 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Move isConstant from ref<> to Expr::Daniel Dunbar
- Ref.h is now freestanding. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72824 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-03Kill off specialized ref<> forwarding methods, in the interest of making it aDaniel Dunbar
more standard reference counting wrapper. - The only interesting changes here are in Ref.h, everything else is just updating foo.method to use foo->method instead. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72777 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-03Remove ref<>'s constant Expr optimization.Daniel Dunbar
- This simplifies what users of the Expr language need to deal with, and paves the way for arbitrary bit-width constant support. - The downside is that concrete interpretation just got *way* slower (2-3x). However, I have a plan for fixing this that should give us the best of both worlds in terms of performance & simplicity. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72753 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-03Fix bug I just introduced, ConstantExpr::computeHash needs to update theDaniel Dunbar
hashValue. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72752 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-03Update ConstantExpr::fromMemory to return a ref<Expr>.Daniel Dunbar
- This function should go away... git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72751 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-03Remove a usage of the direct ref<Expr> constructor that I missed.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72750 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-03Inline Expr::hashConstant into callers.Daniel Dunbar
(Extraneous uses are going away shortly) git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72749 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-03Update a few things that got forgotten in the great "bout" to "ktest"Daniel Dunbar
renaming of '08. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72748 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-02Use ConstantExpr::alloc instead of ref<Expr> directlyDaniel Dunbar
- The "constant optimization" embedded inside ref<Expr> is going away. - No functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72730 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-01Kill off klee_malloc_n, we don't want to support this.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72693 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-01Modify eval() to return a cell reference instead of its contents.Daniel Dunbar
Add get{Dest,Argument}Cell for computing the cell to store instructions results and arguments into, respectuvely. Prep for moving fast path constant evaluation out of the Expr libraary itself. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72692 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-29Changed .ktest header from BOUT\n to KTEST. Old .bout files can still be read.Cristian Cadar
Increased KTEST version. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72592 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-28Small changes to silence some gcc warnings.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72518 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-28Changes to webpage to make both tutorials use the same template.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72515 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-27Unbreak istatsDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72473 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-27Move the regular expression example to "Tutorial Two".Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72472 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-27Some more updates for bout -> ktest renaming.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72471 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-25Add includes to get sprintf (STPBuilder) andDuncan Sands
fprintf, stderr etc (Solver) when compiling with gcc-4.4. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72381 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-25Add include for uint64_t, needed when building withDuncan Sands
gcc-4.4. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72380 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-23Fix for platforms which #define putcharDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72346 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-23Make klee_init_env print some usage instructions with --help.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72338 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-23Changed bout to ktest. Kept "BOUT\n" as the header of test files, for ↵Cristian Cadar
backward compatibility. Also changed KLEE_RUNTEST to KTEST_FILE. Updated tutorial-1. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72312 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-23Renamed klee-bout-tool to ktest-tool.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72306 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-23Updates to install guide and first tutorial.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72305 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-22Improve lex support, apparently FreeBSD lex expects -o to take a joinedDaniel Dunbar
argument. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72271 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-22Add missing include (for FreeBSD build)Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72270 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-22Add "name" argument to klee_make_symbolic, and kill off klee_make_symbolic_name.Daniel Dunbar
- For compatibility we still accept 2 argument form of klee_make_symbolic, but this will go away eventually. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72265 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-22Some minor web page tweaks.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72247 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-22Look for Makefile.rules in the right directory.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72246 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-21Start basic Regexp.c example for klee.Daniel Dunbar
- A few other web page tweaks. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72215 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-21Started web pages describing the main KLEE tools, and the main filesCristian Cadar
generated by KLEE. Small updates to the CSS file and tutorials.html git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72208 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-21Added a first KLEE tutorial.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72207 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-21Missed a couple testsDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72206 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-21Initial KLEE checkin.Daniel Dunbar
- Lots more tweaks, documentation, and web page content is needed, but this should compile & work on OS X & Linux. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-20Web page changes. Added a nice way to format code (div.code) in our CSS file.Cristian Cadar
Added download and install instructions, and a bug report page. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72163 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-19Added empty www/tutorials.html page (test commit to klee repository).Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72123 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-12Add a few useful linksDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@71546 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-08More or less a test commit.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@71231 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-08Make menu work w/o being at the top level.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@71228 91177308-0d34-0410-b5e6-96231b3b80d8
2009-03-15Also point at the stanford checking group webpage.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@67020 91177308-0d34-0410-b5e6-96231b3b80d8
2009-03-15Stub out klee project.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@67019 91177308-0d34-0410-b5e6-96231b3b80d8