Skip to content

Commit 3455f98

Browse files
committed
Fix test information regarding default caching
1 parent 89ac5ca commit 3455f98

File tree

3 files changed

+2
-10
lines changed

3 files changed

+2
-10
lines changed

regression/cbmc/dereference-cache-flag/test-no-cache.desc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,7 @@ test.c
77
--
88
--
99
This is just checking that the --symex-cache-dereferences flag actually turns
10-
dereference caching on and off. Note that dereference caching is turned ON
11-
by default in tests just to make sure that it doesn't break anything.
10+
dereference caching on and off.
1211

1312
I would like to match the expression more precisely, but the order of
1413
comparisons for address of depends on platform-specific logic (unordered_xxx),

regression/cbmc/dereference-cache-flag/test-with-cache.desc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,5 +7,4 @@ symex::dereference_cache!0#1 = 0
77
--
88
--
99
This is just checking that the --symex-cache-dereferences flag actually
10-
turns dereference caching on Note that dereference caching is turned ON
11-
by default in tests just to make sure that it doesn't break anything.
10+
turns dereference caching on.

regression/cbmc/double_deref/README

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -25,9 +25,3 @@ double_deref_with_cast.desc -- a double-deref with an intervening cast (*(int*)*
2525
double_deref_with_member.desc -- a double-deref with an intervening member expression (p->field1->field2), should use a let-expression
2626
double_deref_with_pointer_arithmetic.desc -- a double-deref with intervening pointer arithmetic (p[idx1][idx2]), should use a let-expression
2727
*_single_alias.desc -- variants of the above where the first dereference points to a single possible object, so no let-expression is necessary
28-
29-
Why no-dereference-cache?
30-
-------------------------
31-
32-
Because these tests test for specific VCCs to do with multiple nested complex
33-
dereferences and the dereference caching rewrites these.

0 commit comments

Comments
 (0)