Skip to content

Commit

Permalink
fix test file
Browse files Browse the repository at this point in the history
  • Loading branch information
jcp19 committed Jan 29, 2025
1 parent 9b38dd6 commit a758613
Showing 1 changed file with 1 addition and 10 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -20,25 +20,18 @@ func (t T) Error() string
// if the type of the value on the rhs is a subtype of the type of the LHS
var _ defs.I = (*T)(nil)

/* HERE
// The following is disallowed, as we may use this to get access to a variable of type
// defs.I and, through a call, assume an invariant that does not hold yet
//:: ExpectedOutput(type_error)
var A defs.I = (*T)(nil)
//:: ExpectedOutput(type_error)
var B = defs.I((*T)(nil))



type ItfPkg interface {
decreases
F()
}



HERE */

mayInit
decreases
func initFun1() {
Expand All @@ -49,7 +42,6 @@ func initFun1() {
var i defs.I = T{}
}

/*HERE
mayInit
ensures false
decreases
Expand Down Expand Up @@ -77,5 +69,4 @@ func initFun4() {
// May not open package invariants on a function that may be called during init
//:: ExpectedOutput(type_error)
openDupPkgInv
}
HERE */
}

0 comments on commit a758613

Please sign in to comment.