Merge branch 'master' into feat-at-attributes-1

Source/DafnyCore/AST/Members/ConstantField.cs

@@ -25,10 +25,7 @@ public override bool CanBeRevealed() {
  return true;
  }
 
- public bool ContainsHide {
- get => throw new NotSupportedException();
- set => throw new NotSupportedException();
- }
+ public bool ContainsHide { get; set; }
 
  public new bool IsGhost { get { return this.isGhost; } }
  public List<TypeParameter> TypeArgs { get { return new List<TypeParameter>(); } }

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -2236,8 +2236,11 @@ protected override void EmitNew(Type type, IToken tok, CallStmt initCall /*?*/,
  if (cl is TraitDecl { IsObjectTrait: true }) {
  wr.Write("_dafny.New_Object()");
  } else {
+ var ctor = (Constructor)initCall?.Method; // correctness of cast follows from precondition of "EmitNew"
+ var sep = "";
  wr.Write("{0}(", TypeName_Initializer(type, wr, tok));
  EmitTypeDescriptorsActuals(TypeArgumentInstantiation.ListFromClass(cl, type.TypeArgs), tok, wr);
+ wr.Write(ConstructorArguments(initCall, wStmts, ctor, sep));
  wr.Write(")");
  }
  }

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/constantWithReveal.dfy

@@ -0,0 +1,8 @@
+// RUN: %verify %s &> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+opaque function Foo(x: int): int {
+ x
+}
+
+const C := reveal Foo(); Foo(42)

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/constantWithReveal.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Class.java

@@ -2,7 +2,7 @@
 
 import java.math.BigInteger;
 
-public class Class extends _ExternBase_Class {
+public class Class {
  private final BigInteger n;
 
  public Class(BigInteger n) {

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.go

@@ -17,12 +17,6 @@ func (obj *Class) Get() dafny.Int {
  return obj.n
 }
 
-// have to implement this because the Go backend can't mix Dafny and Go code :-\
-
-func (obj *Class) Print() {
- fmt.Printf("My value is %d\n", obj.n)
-}
-
 type CompanionStruct_Class_ struct{}
 var Companion_Class_ = CompanionStruct_Class_{}
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.py

@@ -17,8 +17,3 @@ def SayHi():
 
  def Get(self):
  return self.n
-
- def Print(self):
- _dafny.print(_dafny.string_of(_dafny.Seq("My value is ")))
- _dafny.print(_dafny.string_of((self).Get()))
- _dafny.print(_dafny.string_of(_dafny.Seq("\n")))

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy

@@ -1,24 +1,23 @@
 // RUN: %run --target cs "%s" --input %S/ExternCtors-externs/Library.cs > "%t"
 // RUN: %run --target java "%s" --input %S/ExternCtors-externs/Class.java >> "%t"
 // RUN: %run --target py "%s" --input %S/ExternCtors-externs/Library.py >> "%t"
+// RUN: %run --target go "%s" --input %S/ExternCtors-externs/Library.go >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
-// FIXME: Extern constructors are currently broken in Go and JavaScript,
-// so they are omitted
+// FIXME: Extern constructors are currently broken in JavaScript,
+// so that is omitted
 
 method Main() {
  Library.Class.SayHi();
  var obj := new Library.Class(42);
- obj.Print();
+ print "My value is ", obj.Get(), "\n";
 }
 
 module {:extern "Library"} Library {
  class {:extern} Class {
  constructor {:extern} (n: int)
  static method {:extern} SayHi()
  function {:extern} Get() : int
- method Print() {
- print "My value is ", Get(), "\n";
- }
  }
 }
+

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy.expect

@@ -10,3 +10,7 @@ My value is 42
 Dafny program verifier finished with 1 verified, 0 errors
 Hello!
 My value is 42
+
+Dafny program verifier finished with 1 verified, 0 errors
+Hello!
+My value is 42

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify "%s" --performance-stats=10 --relax-definite-assignment --allow-axioms > "%t"
+// RUN: %exits-with 4 %verify "%s" --performance-stats=100 --relax-definite-assignment --allow-axioms > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module AssignmentToNat {

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect

@@ -91,5 +91,5 @@ SubsetTypes.dfy(459,15): Error: assertion might not hold
 SubsetTypes.dfy(464,13): Error: assertion might not hold
 
 Dafny program verifier finished with 13 verified, 91 errors
-Total resources used is 774980
-Max resources used by VC is 101850
+Total resources used is 775000
+Max resources used by VC is 101900

docs/dev/news/5761.feat

@@ -0,0 +1 @@
+Added opaque blocks to the language. Opaque blocks enable improving verification performance. See the documentation for more details.

docs/dev/news/5779.feat

@@ -0,0 +1 @@
+By blocks ("... by { ... }") are now available for assert statements, call statements, and the three types of assignments (:=, :-, :|). Also, by blocks should now be more intuitive since they enable proving any assertions on the left-hand side of the 'by', not just the 'outermost' one. For example, previously `assert 3 / x == 1 by { assume x == 3; }` could still give a possible division by zero error, but now it won't. 

docs/dev/news/5823.fix

@@ -0,0 +1 @@
+Fix a bug that prevented using reveal statement expressions in the body of a constant.