From 0c1ec594e68dab4fcd458a00f9f7a1ac6de2e218 Mon Sep 17 00:00:00 2001 From: leino Date: Mon, 28 Sep 2015 13:16:15 -0700 Subject: Changed computation of ghosts until pass 2 of resolution. Other clean-up in resolution passes, like: Include everything of type "char" into bounds that are discovered, and likewise for reference types. Allow more set comprehensions, determining if they are finite based on their argument type. Changed CalcExpr.SubExpressions to not include computed expressions. --- Test/dafny0/CallStmtTests.dfy.expect | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Test/dafny0/CallStmtTests.dfy.expect') diff --git a/Test/dafny0/CallStmtTests.dfy.expect b/Test/dafny0/CallStmtTests.dfy.expect index 8a334754..246b89f8 100644 --- a/Test/dafny0/CallStmtTests.dfy.expect +++ b/Test/dafny0/CallStmtTests.dfy.expect @@ -1,3 +1,3 @@ -CallStmtTests.dfy(6,3): Error: LHS of assignment must denote a mutable variable -CallStmtTests.dfy(17,10): Error: actual out-parameter 0 is required to be a ghost variable +CallStmtTests.dfy(7,4): Error: LHS of assignment must denote a mutable variable +CallStmtTests.dfy(20,11): Error: actual out-parameter 0 is required to be a ghost variable 2 resolution/type errors detected in CallStmtTests.dfy -- cgit v1.2.3