diff options
| author | Daniel Dunbar <daniel@zuster.org> | 2009-06-07 07:36:26 +0000 |
|---|---|---|
| committer | Daniel Dunbar <daniel@zuster.org> | 2009-06-07 07:36:26 +0000 |
| commit | 24e065075e7ec973db84639725696b9f84975b2f (patch) | |
| tree | 83d77fb2ea51bd12745567fbabc9c3b1936391d4 /www | |
| parent | 98633b8240294910f74877e4c8b992bc5669ada1 (diff) | |
| download | klee-24e065075e7ec973db84639725696b9f84975b2f.tar.gz | |
Eliminate anonymous versions.
- For now, this means the isRooted flag for arrays isn't propogated to the
kquery language. We should figure out how to do this, but allow anonymous
versions isn't the right way.
Also, improved the error on invalid writes a bit.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73018 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'www')
| -rw-r--r-- | www/KQuery.html | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/www/KQuery.html b/www/KQuery.html index 4f613c4e..db0d2b59 100644 --- a/www/KQuery.html +++ b/www/KQuery.html @@ -317,8 +317,7 @@ <p><b>Syntax:</b></p> <div class="syntax"> - version = identifier<br> - version = "[" [ update-list ] "]" [ "@" version "]"<br> + version = identifier | "[" [ update-list ] "]" "@" version<br> update-list = lhs-expression "=" rhs-expression [ "," update-list ]<br> </div> @@ -327,8 +326,6 @@ of writes which are to be concatenated to another version (the most recent writes are first).</p> - <p>FIXME: Get rid of anonymous arrays.</p> - <h2><a name="exprs">Expressions</a></h2> <p>Expressions are strongly typed, and have the following general |