cleaned up examples

uuverifiers · Oct 15, 2020 · e1ab123 · e1ab123
1 parent 213f829
commit e1ab123
Show file tree

Hide file tree

Showing 26 changed files with 4 additions and 131 deletions.
diff --git a/heap-theory-examples/unsafe-access-001.c → heap-theory-examples/invalid-access.c b/heap-theory-examples/unsafe-access-001.c → heap-theory-examples/invalid-access.c
diff --git a/...heory-examples/unsafe-access-001.c-1.smt2 → heap-theory-examples/invalid-access.smt2 b/...heory-examples/unsafe-access-001.c-1.smt2 → heap-theory-examples/invalid-access.smt2
diff --git a/heap-theory-examples/list-002-fail.c → heap-theory-examples/list-002-unsafe.c b/heap-theory-examples/list-002-fail.c → heap-theory-examples/list-002-unsafe.c
diff --git a/heap-theory-examples/list-002-fail.c-1.smt2 → heap-theory-examples/list-002-unsafe.smt2 b/heap-theory-examples/list-002-fail.c-1.smt2 → heap-theory-examples/list-002-unsafe.smt2
diff --git a/heap-theory-examples/list-004.c-1.smt2 → heap-theory-examples/list-004.smt2 b/heap-theory-examples/list-004.c-1.smt2 → heap-theory-examples/list-004.smt2
diff --git a/heap-theory-examples/mutually-referential-structs-fail.c b/heap-theory-examples/mutually-referential-structs-fail.c
diff --git a/...ually-referential-structs-unsafe.c-1.smt2 → .../mutually-referential-structs-unsafe.smt2 b/...ually-referential-structs-unsafe.c-1.smt2 → .../mutually-referential-structs-unsafe.smt2
diff --git a/heap-theory-examples/mutually-referential-structs.c b/heap-theory-examples/mutually-referential-structs.c
@@ -20,5 +20,5 @@ void main()
 
   struct parent *cp1 = list->child1->p;
   struct parent *cp2 = list->child2->p;
-  assert(cp1 == list || cp1 == 0);
+  assert(list->child1->p == list);
 }
diff --git a/...utually-referential-structs-fail.c-1.smt2 → ...xamples/mutually-referential-structs.smt2 b/...utually-referential-structs-fail.c-1.smt2 → ...xamples/mutually-referential-structs.smt2
diff --git a/...-theory-examples/opassign-struct.c-1.smt2 → heap-theory-examples/opassign-struct.smt2 b/...-theory-examples/opassign-struct.c-1.smt2 → heap-theory-examples/opassign-struct.smt2
diff --git a/heap-theory-examples/simple-arith.c b/heap-theory-examples/simple-arith.c
@@ -5,7 +5,7 @@ void main() {
     *x = 3;
     int y = *x + *x;
     assert(y == 0 || y == 3 || y == 6 || y == 42 || y == 45 || y == 84);
-    /* possible values for y without refinements
+    /* possible values for y using the invariant encoding without refinements
       0  +  0 = 0
       0  +  3 = 3
       3  +  3 = 6

diff --git a/heap-theory-examples/simple-arith.c-1.smt2 → heap-theory-examples/simple-arith.smt2 b/heap-theory-examples/simple-arith.c-1.smt2 → heap-theory-examples/simple-arith.smt2
diff --git a/...-theory-examples/simple-struct-2.c-1.smt2 → heap-theory-examples/simple-struct-2.smt2 b/...-theory-examples/simple-struct-2.c-1.smt2 → heap-theory-examples/simple-struct-2.smt2
diff --git a/heap-theory-examples/simple-struct.c-1.smt2 → heap-theory-examples/simple-struct.smt2 b/heap-theory-examples/simple-struct.c-1.smt2 → heap-theory-examples/simple-struct.smt2
diff --git a/...ory-examples/stackptr-to-heapptr.c-1.smt2 → ...-theory-examples/stackptr-to-heapptr.smt2 b/...ory-examples/stackptr-to-heapptr.c-1.smt2 → ...-theory-examples/stackptr-to-heapptr.smt2
diff --git a/heap-theory-examples/swap-1-fail.c b/heap-theory-examples/swap-1-fail.c
diff --git a/heap-theory-examples/swap-1.c b/heap-theory-examples/swap-1.c
@@ -9,6 +9,6 @@ void main() {
     int *b = calloc(sizeof(int));
     *b = 42;
     swap(&a, b);
-    assert(a == 0 || a == 3 || a == 42);
+    assert(a == 42);
 }
 
diff --git a/heap-theory-examples/swap-1.c-1.smt2 b/heap-theory-examples/swap-1.c-1.smt2
diff --git a/heap-theory-examples/swap-1-fail.c-1.smt2 → heap-theory-examples/swap-1.smt2 b/heap-theory-examples/swap-1-fail.c-1.smt2 → heap-theory-examples/swap-1.smt2
diff --git a/heap-theory-examples/swap-2-fail.c b/heap-theory-examples/swap-2-fail.c
diff --git a/heap-theory-examples/swap-2.c b/heap-theory-examples/swap-2.c
@@ -11,6 +11,6 @@ void main() {
     *b = 42;
     swap(a, b);
     int tmp = *a;
-    assert(tmp == 0 || tmp == 3 || tmp == 42);
+    assert(tmp == 42);
 }
 
diff --git a/heap-theory-examples/swap-2-fail.c-1.smt2 → heap-theory-examples/swap-2.smt2 b/heap-theory-examples/swap-2-fail.c-1.smt2 → heap-theory-examples/swap-2.smt2
diff --git a/heap-theory-examples/swap-3.c-1.smt2 b/heap-theory-examples/swap-3.c-1.smt2
diff --git a/heap-theory-examples/swap-2.c-1.smt2 → heap-theory-examples/swap-3.smt2 b/heap-theory-examples/swap-2.c-1.smt2 → heap-theory-examples/swap-3.smt2
diff --git a/...theory-examples/typecastSafe-001.c-1.smt2 → heap-theory-examples/typecastSafe-001.smt2 b/...theory-examples/typecastSafe-001.c-1.smt2 → heap-theory-examples/typecastSafe-001.smt2
diff --git a/...eory-examples/typecastUnsafe-001.c-1.smt2 → heap-theory-examples/typecastUnsafe-001.smt2 b/...eory-examples/typecastUnsafe-001.c-1.smt2 → heap-theory-examples/typecastUnsafe-001.smt2