From 8cc9f82219a818ef54dda2c59b3a56d07114c3fb Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 21 Sep 2012 14:46:50 -0700 Subject: DafnyExtension: adding some missing keywords (for imports) --- Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index 19f98ff7..ec1514ae 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -227,6 +227,7 @@ namespace DafnyLanguage #region keywords case "allocated": case "array": + case "as": case "assert": case "assume": case "bool": @@ -250,7 +251,7 @@ namespace DafnyLanguage case "function": case "ghost": case "if": - case "imports": + case "import": case "in": case "int": case "invariant": @@ -265,6 +266,7 @@ namespace DafnyLanguage case "null": case "object": case "old": + case "opened": case "parallel": case "predicate": case "print": -- cgit v1.2.3 From 42e28fd3c37ea4bd49d8c237e0233d2964e82cf3 Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 24 Sep 2012 10:21:32 +0200 Subject: added output for a test case --- Chalice/tests/predicates/LinkedList-various.output.txt | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 Chalice/tests/predicates/LinkedList-various.output.txt diff --git a/Chalice/tests/predicates/LinkedList-various.output.txt b/Chalice/tests/predicates/LinkedList-various.output.txt new file mode 100644 index 00000000..a8a90bb8 --- /dev/null +++ b/Chalice/tests/predicates/LinkedList-various.output.txt @@ -0,0 +1,4 @@ +Verification of LinkedList-various.chalice using parameters="" + + +Boogie program verifier finished with 0 errors and 0 smoke test warnings -- cgit v1.2.3