DeforaNetworks/deepstate
3
0
Fork 0
Code Releases Activity

Refactored to split common code between Manticore and Angr out into common.py. Implemented the new deferred streaming stuff, it seems to work semi-well for this simple cases I've tested, but there's still work to do. The latest code has some remaining issues. Printing out the final input bytes in Angr shows the wrong thing, although what gets streamed out is right. This is visible when running mctest-angr examples/ArtihmeticProperties. With Manticore, the big issue is that it doesn't properly pickle smt expressions (or something to this effect), so I'm ending up with multiple definitions of the same stuff and that throws exceptions. This is tricky to deal with because the streaming of output needs to be able to save symbolic data.

Browse Source
This commit is contained in:
Peter Goodman
2017-11-01 02:42:31 -04:00
parent 8ec44074ad
commit a46e06b03b
18 changed files with 1765 additions and 495 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
examples/ArithmeticProperties.cpp
View File

@@ -39,7 +39,8 @@ TEST(Arithmetic, AdditionIsAssociative) {
TEST(Arithmetic, InvertibleMultiplication_CanFail) {
ForAll<int, int>([] (int x, int y) {
ASSUME_NE(y, 0);
ASSUME_NE(y, 0)
<< "Assumed non-zero value for y: " << y;
ASSERT_EQ(x, (x / y) * y)
<< x << " != (" << x << " / " << y << ") * " << y;
});