Skip to content

Commit 54389a9

Browse files
committed
Move README information into test desc files
1 parent 561a73e commit 54389a9

File tree

3 files changed

+6
-6
lines changed

3 files changed

+6
-6
lines changed

regression/cbmc/dereference-cache-flag/README.md

Lines changed: 0 additions & 1 deletion
This file was deleted.

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@ test.c
66
^SIGNAL=0$
77
--
88
--
9-
Note that dereference caching is turned ON by default
10-
in tests just to make sure that it doesn't break
11-
anything.
9+
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.
1212

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

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,5 +6,6 @@ symex::dereference_cache!0#1 = 0
66
^SIGNAL=0$
77
--
88
--
9-
Note that dereference caching is turned ON by default in
10-
tests just to make sure that it doesn't break anything.
9+
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.

0 commit comments

Comments
 (0)