Pull request 🔀 created by bitbucket user evolutics on 2013-05-22 21:35
Last updated on 2013-05-22 22:34
Original Bitbucket pull request id: 4

Participants:

• bitbucket user bbrodowsky ✔️

Source: unknown commit on branch default of an unknown repo
Destination: ccb3d62 on branch master

State: MERGED

A couple of improved details. Most importantly for the induction part, quantifications over multiple variables are now documented in the SIL grammar.

Created by @alexanderjsummers on 2013-09-04 10:09
Last updated on 2017-03-07 16:46

It's confusing that
var x : Seq[Int] := Seq()
type-checks (because the required type is inferred), but
assert x == Seq()
causes a type-error (which is also currently an exception).
In the latter case, the type needs to be specified manually:

#!scala
assert x == Seq[Int]()

Instead, it would be better to allow the empty sequence to have a polymorphic type, which can match any sequence type.

Attachments:

• 0018.sil

Created by @alexanderjsummers on 2013-09-01 23:59
Last updated on 2014-05-07 14:08

writing acc(root.valid,write)
instead of
acc(root.valid(),write)

causes a class-cast exception (attempting to cast Predicate to Field)

Attachments:

• bad_predicate.sil

Pull request 🔀 created by bitbucket user severinh on 2013-11-27 13:26
Last updated on 2013-12-04 12:48
Original Bitbucket pull request id: 12

Participants:

• @mschwerhoff (reviewer)
• bitbucket user severinh

Source: unknown commit on branch default of an unknown repo
Destination: 5aa751d on branch master

State: DECLINED

There is also a unit test, just in case. ;-)

Created by bitbucket user severinh on 2013-10-29 10:39
Last updated on 2013-11-20 17:17

The parser fails to recognize two consecutive inhale statements if they are not separated by a semicolon.

The type of error depends on whether the inhale expression is wrapped with parentheses:

method foo()
{
  inhale (true)
  inhale (true) // "hale not defined."
}

method foo()
{
  inhale true
  inhale true // "Parse error: Failure: `.' expected but `}' found"
}

Using a different keyword for either "inhale" or "in" causes the problem to disappear. But this is obviously not what we want. ;-)

It seems that debugging the parser is rather difficult. Any ideas of what the problem could be?

Created by @mschwerhoff on 2013-06-03 15:29
Last updated on 2014-05-28 12:33

Parsing the Sil program

method test01() {
  assert |Seq()| == 0
}

yields an AST in which Seq() is represented as an EmptySeq whose typ.elementType is a TypeVar.

It appears to be ok to type it as an empty sequence over Ref or Int, or any other type for that matter, although it is not really a clean solution.

Pull request 🔀 created by bitbucket user evolutics on 2013-05-03 11:17
Last updated on 2013-05-03 11:58
Original Bitbucket pull request id: 1

Participants:

• @mschwerhoff ✔️
• bitbucket user stefanheule ✔️

Source: unknown commit on branch default of an unknown repo
Destination: 2a5c5b8 on branch master

State: MERGED

• The first part is a generalization of the expression transformer to make both pre- and postprocessing of the current expression possible. Moreover, the recursion on the subexpressions depends on a predicate. The partial functions have just Exp as a codomain instead of Option[Exp], since they are partial anyway; correct me if you have something else in mind.
• The second part is a function to simplify expressions, which I find useful for automatically generated SIL code. Use it with care. Alternatively, I can keep it in my project if you do not need it here.

Pull request 🔀 created by bitbucket user Korbinian Breu on 2014-01-18 13:43
Last updated on 2014-01-20 12:59
Original Bitbucket pull request id: 18

Participants:

• @mschwerhoff (reviewer)

Source: c9669fa on branch pw-korbinian-breu/sil_forallfix/default
Destination: 332e7fe on branch master

State: MERGED

Created by @mschwerhoff on 2013-07-30 09:17
Last updated on 2013-11-19 16:57

Type checking the following (probably non-minimal) program

var f: Int
var b: Bool

predicate P(this: Ref) {
     acc(this.b, write)
  && (this.b ==> acc(this.f, write))
}

method branch(this: Ref)
  requires acc(this.P(), write)
{
  assert
       (3 > 2)
    && (unfolding acc(this.P(), write)
          in (!this.b ? true : true))    // HERE
}

fails with

expected Ref, but got Bool (branch.sil:HERE)
expected Bool, but got Ref (branch.sil:HERE)

Replacing the ite-guard !this.b with the equivalent (this.b == false) or with the nonequivalent this.b makes the program type-check.

Pull request 🔀 created by bitbucket user severinh on 2013-12-25 12:58
Last updated on 2013-12-25 14:32
Original Bitbucket pull request id: 16

Participants:

• @alexanderjsummers ✔️

Source: unknown commit on branch default of an unknown repo
Destination: 6ad6563 on branch master

State: MERGED

Pull request 🔀 created by bitbucket user severinh on 2013-11-27 12:37
Last updated on 2013-11-27 12:59
Original Bitbucket pull request id: 11

Participants:

• @mschwerhoff ✔️
• bitbucket user severinh
• @alexanderjsummers (reviewer)

Source: unknown commit on branch default of an unknown repo
Destination: 886e12f on branch master

State: MERGED

If you prefer, I can move the CFG transformation code to a separate file like CFGTransformer.scala.

Created by @mschwerhoff on 2013-11-03 13:26
Last updated on 2014-06-18 17:07

The program

var f: Int

function f(): Bool { true }

method m(x: Ref)
  requires acc(x.f, write)
{}

results in the unnecessarily technical error message

expected identifier, but got PFunction(PIdnDef(f),List(),Bool,List(),List(),PBoolLit(true)).

Created by bitbucket user Korbinian Breu on 2013-11-06 12:56
Last updated on 2013-11-06 13:20

The following piece of code

#!scala

var s:Set[Ref]

predicate inv(this: Ref)
{
    !(null in this.s)
}

is not parsed correctly, in seems to have precedence before the dot "."

#!scala

[info]   expected Ref, but got Bool (issue.sil:5) (issue.sil:5)
[info]   expected one of [Set[.], Multiset[.], Seq[.]], but got Ref (issue.sil:5) (issue.sil:5)
[info]   expected Bool, but got Set[Ref] (issue.sil:5) (issue.sil:5) (SilSuite.scala:246)

Pull request 🔀 created by bitbucket user evolutics on 2013-06-05 09:57
Last updated on 2013-06-05 15:10
Original Bitbucket pull request id: 6

Source: unknown commit on branch default of an unknown repo
Destination: 7c5dac6 on branch master

State: MERGED

This corrects my mistake in the node transformer about indefinite recursions. In the nodes FieldAccess and PredicateAccess, the transformer should not recurse on the accessed field and predicate, respectively. If so, this can in turn contain such a node, thereby causing a stack overflow.

Created by @mschwerhoff on 2013-06-05 15:12
Last updated on 2014-05-07 13:44

The following Sil program passes the type checker, although next in acc(next.valid, write) is undefined.

var item: Int
var next: Ref

predicate valid(this: Ref) {
     acc(this.item, write)
  && acc(this.next, write)
  && (this.next != null ==> acc(next.valid, write))
}

Created by @alexanderjsummers on 2013-09-01 22:51
Last updated on 2013-11-19 22:13

var value: Int;

causes a parse error, due to the semicolon being unexpected. I think it would be nicer to make the symbol optional, as in Chalice, especially for users unfamiliar with the language.

Created by @alexanderjsummers on 2013-12-12 14:26
Last updated on 2014-05-07 14:45

Leaving an empty parameter list for a predicate definition causes a "head of empty list" exception to be thrown when the predicate is used (inhaled) in an assertion.

Attachments:

• 0031.sil

Created by @alexanderjsummers on 2013-09-01 23:02
Last updated on 2013-09-01 23:30

(true <==> true) cannot be parsed (at least, as the body of a predicate), whereas (true ==> true) works fine. <==> is the correct symbol for "iff", according to Parser.scala

Pull request 🔀 created by bitbucket user evolutics on 2013-07-03 11:33
Last updated on 2013-07-15 14:06
Original Bitbucket pull request id: 7

Participants:

• bitbucket user stefanheule ✔️

Source: unknown commit on branch default of an unknown repo
Destination: 2a0bf7a on branch master

State: MERGED

Correction of my own code about transformation of specifications. It now correctly generates statements instead of expressions.

Pull request 🔀 created by bitbucket user severinh on 2013-12-04 12:47
Last updated on 2013-12-04 12:50
Original Bitbucket pull request id: 13

Participants:

• @mschwerhoff (reviewer) ✔️

Source: unknown commit on branch simplify-shallow-copy of an unknown repo
Destination: 5aa751d on branch master
Marge commit: 0b7a0c2

State: MERGED

Thanks for your suggestion Malte. It definitely makes sense.

For some reason, Bitbucket did not allow me to change the branch from which to pull commits, which is why I created a new pull request. The reason why I needed to create a new branch was because my default branch already contains other commits.

Created by @alexanderjsummers on 2013-09-01 23:48
Last updated on 2014-05-08 13:07

When declaring a field as

var f: int

a requirement failure occurs, with a stack trace (it should be "Int"). It would be better to get a message indicating the probable cause.

Created by @alexanderjsummers on 2013-09-04 10:23
Last updated on 2014-01-22 13:16

Reusing the same quantified variable in the same scope is not supported: it yields an error that the variable is "already defined", the second time.

Attachments:

• 0019.sil

Created by @mschwerhoff on 2013-11-20 13:14
Last updated on 2014-06-18 17:06

Sequence append can also be applied to sets, as done in this snippet:

method test(x: Set[Int]) returns (y: Set[Int]) {
  y := x ++ x
}

As far as I know ++ is not overloaded; union should be used for sets.

Pull request 🔀 created by @mschwerhoff on 2013-05-17 11:51
Last updated on 2013-05-17 11:52
Original Bitbucket pull request id: 3

Source: unknown commit on branch default of an unknown repo
Destination: 988f3e8 on branch master
Marge commit: eb1f48f

State: MERGED

• Fixed a bug in DomainMember.equals
• Added functions for collecting (free) type variables
• Added test cases for domain handling

Created by @alexanderjsummers on 2013-12-11 17:26
Last updated on 2017-11-24 18:11

For a Perm-typed field, it should be possible to use the field value as the second parameter in an acc(.., ..) construct. However, this is rejected.

(this behaviour is seen in test-case all\permissions\epsilons.sil more indirectly, through an unfolding of a predicate, but that case is currently ignored by Silicon).

Attachments:

• 0030.sil

Created by @mschwerhoff on 2013-07-30 08:52
Last updated on 2013-11-19 16:57

The program

var b: Bool

predicate P(this: Ref) { acc(this.b, write) }

method branch(this: Ref)
  requires acc(this.P, write)
{}

makes the parser crash with

java.lang.ClassCastException: semper.sil.ast.Predicate cannot be cast to semper.sil.ast.Field
[info]   at semper.sil.parser.Translator.findField(Translator.scala:106)
[info]   at semper.sil.parser.Translator.semper$sil$parser$Translator$$exp(Translator.scala:267)
[info]   at semper.sil.parser.Translator.semper$sil$parser$Translator$$exp(Translator.scala:316)
[info]   at semper.sil.parser.Translator$$anonfun$semper$sil$parser$Translator$$translate$1.apply(Translator.scala:43)
[info]   at semper.sil.parser.Translator$$anonfun$semper$sil$parser$Translator$$translate$1.apply(Translator.scala:43)
[info]   at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:244)
[info]   at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:244)
[info]   at scala.collection.immutable.List.foreach(List.scala:318)
[info]   at scala.collection.TraversableLike$class.map(TraversableLike.scala:244)
[info]   at scala.collection.AbstractTraversable.map(Traversable.scala:105)
[info]   ...

If the requires-clause is changed to

requires acc(P(this), write)

then the following parser error is reported:

Parse error: Failure: '.' expected but ',' found

Created by bitbucket user Korbinian Breu on 2013-09-04 14:21
Last updated on 2013-09-04 18:04

The exception in the title occurs randomly when I run tests with sbt. Is there any workaround to increase this "PermGen" space?

Created by @mschwerhoff on 2013-05-29 09:21
Last updated on 2013-11-19 16:57

Consider the following program (take from Sil:all/basic/permissions_epsilons.sil):

var f: Ref
var p: Perm

method test6(this: Ref)
  requires this != null && acc(this.f, 50/100)
  ensures acc(this.f, 51/100 + epsilon)
{
  exhale acc(this.f, 3 * write)
  exhale acc(this.f, 3 * epsilon)
  exhale acc(this.f, 2 * epsilon)
  inhale acc(this.f, 1/100)             /* L1*/
  inhale acc(this.f, epsilon + epsilon) /* L2 */
  exhale acc(this.f, epsilon)           /* L3 */
  inhale acc(this.f, epsilon * 5)
}

Parsing it yields Parse error: Failure: '.' expected but 'i' found reported for line L2.

Commenting L1 yields Parse error: Failure: '.' expected but 'e' found reported for line L3.

Commenting L2 as well finally satisfies the parser.

Strangely, if the program is reduced to (with one of the lines uncommented)

var f: Ref
var p: Perm

method test(this: Ref) {
  // inhale acc(this.f, 1/100)
  // inhale acc(this.f, epsilon + epsilon)
}

then the parser is satisfied right away. It could thus very well be that the culprit won't be found in L1 or L2.

Created by bitbucket user Korbinian Breu on 2014-01-18 13:53
Last updated on 2014-01-20 13:09

Hi,

the following program does not parse correctly, only identifiers seem to be allowed for an assignment to new:

#!scala

var f:Ref
method m(o:Ref)
requires acc(o.f, write)
{
    o.f := new()
}

The error is: Parse error: Failure: identifier expected.

Created by @alexanderjsummers on 2013-09-01 23:10
Last updated on 2013-11-19 16:57

(!this.leftDown ==> acc(this.leftValid(),write) )
does not parse, whereas
(this.leftDown ==> acc(this.leftValid(),write) )
does.

I assume this is a bug in the grammar regarding where acc predicates can occur.

(file attached is work in progress)

Attachments:

• AVLTree.iterative.sil

Created by @alexanderjsummers on 2013-09-04 13:09
Last updated on 2013-11-20 08:28

x in S ==> x in T
parses as
x in (S ==> (x in T)).

It seems to me that "in" should have stronger precedence than implication.

Created by bitbucket user evolutics on 2013-05-24 17:15
Last updated on 2013-11-20 08:31

The SIL program

#!scala
method variables()
{
  var number: Int
  var index: Int
  number := 1
  index := 0 // Line 6
}

cannot be parsed. I receive the parse error Failure: identifier expected for line 6.

The problem disappears if I replace the variable name index with another. Alternatively, terminating line 5 with a semicolon ; works as well.

Created by @alexanderjsummers on 2013-09-04 13:35
Last updated on 2017-11-26 13:24

When typing a conditional expression for which the same exact types have not (yet) been inferred for the two latter operands, a requirement failure occurs (with no useful message). This can easily happen with sequences, because of the lack of type information for empty sequences (as in the example attached).

Attachments:

• 0022.sil

Created by @mschwerhoff on 2013-05-24 15:10
Last updated on 2013-11-19 16:57

The binding power of the dot-operator appears to be wrong.

The snippet

#!text
var Node_n: Ref

method test(this: Ref)
  requires this != null && acc(this.Node_n, write)
{
  assert this != this.Node_n
}

yields Parse error: Failure: '.' expected but '}' found.

Replacing the method body with

#!text
  var v: Ref := this.Node_n
  assert this != v

or simply with

#!text
  assert this != this.Node_n

makes the parser happy.

Pull request 🔀 created by bitbucket user severinh on 2013-12-12 11:26
Last updated on 2013-12-16 14:57
Original Bitbucket pull request id: 15

Participants:

• @mschwerhoff ✔️
• bitbucket user severinh

Source: unknown commit on branch default of an unknown repo
Destination: e9e3222 on branch master
Marge commit: b3bf836

State: MERGED

We would like to reuse SIL's testing infrastructure in Sample, because it is much more sophisticated (based on ScalaTest, supports inline annotations, project-specific annotations, annotations for missing/unexpected output etc.).
This changeset cleanly splits the testing infrastructure into a small SIL-specific part and a generic part that is completely independent from the system under test (e.g. verifier) and the underlying AST.

The new infrastructure uses the term 'output' instead of 'error' for output produced by the system under test. While 'error' makes sense when testing verifiers, 'output' is more generic and can also refer to positive output like inferred invariants. As a result, annotations have been renamed from 'ExpectedError' to 'ExpectedOutput' etc.

Furthermore, the meaning of IDs associated with an output has changed slightly. An output is now associated with a mandatory key ID and an optional value ID. The key ID groups the outputs into namespaces/scopes such as 'precondition.violated' or 'sample.inferred.invariant', while the optional value ID may give additional information such as 'insufficient.permission' or 'n>0', respectively.

The interface of SilSuite has not changed at all. Thus, dependent projects like Silicon do not need to be updated.

There are also a couple of unit tests.

Created by @alexanderjsummers on 2013-09-04 13:05
Last updated on 2013-11-20 08:30

For larger examples, character positions would be extremely useful

Pull request 🔀 created by bitbucket user Korbinian Breu on 2013-09-04 15:09
Last updated on 2013-09-04 16:03
Original Bitbucket pull request id: 10

Participants:

• @alexanderjsummers ✔️

Source: fa4b3a2 on branch pw-korbinian-breu/sil/default
Destination: 09b9abe on branch master
Marge commit: df3a991

State: MERGED

Pull request 🔀 created by bitbucket user Korbinian Breu on 2013-08-28 08:16
Last updated on 2013-08-28 14:39
Original Bitbucket pull request id: 9

Source: bd63649 on branch pw-korbinian-breu/sil/default
Destination: 8fb0b4b on branch master

State: MERGED

Created by @mschwerhoff on 2013-05-27 14:51
Last updated on 2013-11-19 16:56

The error Parse error: Failure: '{' expected but 'r' found is thrown for the following snippet taken from the test file Sil:all/basic/while.sil:

while (j < 3)
  invariant r != null
  invariant r.f == 2
    {
        j := j+1
    }

The error disappears when the clauses are merged to invariant r != null && r.f == 2.

Pull request 🔀 created by bitbucket user evolutics on 2013-05-03 13:19
Last updated on 2020-01-23 12:28
Original Bitbucket pull request id: 2

Participants:

• bitbucket user stefanheule ✔️
• @fpoli ✔️

Source: unknown commit on branch default of an unknown repo
Destination: f584241 on branch master
Marge commit: 89f6fb4

State: MERGED

Sorry for the duplicate, but I had trouble with access rights on Bitbucket.

• The first part is a generalization of the expression transformer to make both pre- and postprocessing of the current expression possible. Moreover, the recursion on the subexpressions depends on a predicate. The partial functions have just Exp as a codomain instead of Option[Exp], since they are partial anyway; correct me if you have something else in mind.

• The second part is a function to simplify expressions, which I find useful for automatically generated SIL code. Use it with care. Alternatively, I can keep it in my project if you do not need it here.

Pull request 🔀 created by bitbucket user severinh on 2013-12-05 13:46
Last updated on 2013-12-12 11:14
Original Bitbucket pull request id: 14

Participants:

• @mschwerhoff (reviewer) ✔️
• bitbucket user severinh
• @alexanderjsummers (reviewer)

Source: unidentified commit on branch severinh/sil/generic-test-infrastructure (Mercurial commit was 2a53e4eba176)
Destination: ebbeffa on branch master

State: DECLINED

We would like to reuse SIL's testing infrastructure in Sample, because it is much more sophisticated (based on ScalaTest, supports inline annotations, project-specific annotations, annotations for missing/unexpected output etc.).

This changeset cleanly splits the testing infrastructure into a small SIL-specific part and a generic part that is completely independent from the system under test (e.g. verifier) and the underlying AST.

The new infrastructure uses the term 'output' instead of 'error' for output produced by the system under test. While 'error' makes sense when testing verifiers, 'output' is more generic and can also refer to positive output like inferred invariants. As a result, annotations have been renamed from 'ExpectedError' to 'ExpectedOutput' etc.

Furthermore, the meaning of IDs associated with an output has changed slightly. An output is now associated with a mandatory key ID and an optional value ID. The key ID groups the outputs into namespaces/scopes such as 'precondition.violated' or 'sample.inferred.invariant', while the optional value ID may give additional information such as 'insufficient.permission' or 'n>0', respectively.

The interface of SilSuite has not changed at all. Thus, dependent projects like Silicon do not need to be updated.

There are also a couple of unit tests.

I'm open for any suggestions for further improvements.

Pull request 🔀 created by bitbucket user evolutics on 2013-07-16 14:27
Last updated on 2013-07-21 21:20
Original Bitbucket pull request id: 8

Participants:

• bitbucket user evolutics
• bitbucket user stefanheule (reviewer) ✔️

Source: unknown commit on branch default of an unknown repo
Destination: bcaf7e7 on branch master

State: MERGED

As decided during the Semper meeting on 6 June 2013, inhale exhale expressions can appear in quantified expressions. This is the third and last point of the corresponding meeting in the archive, which can be found here:
https://bitbucket.org/semperproject/documentation/wiki/Semper%20Meeting%20Archive

For example, it should be possible to have code like ensures forall integer: Int :: […, …], where […, …] is an inhale exhale expression.

Moreover, the Kiama library is urgently updated to its latest version 1.5.1. Pretty-printing in earlier versions like 1.5.0 uses too much stack for some programs, causing the stack to overflow. This is now fixed, as documented here: http://wiki.kiama.googlecode.com/hg/doc/1.5.1/notes.html

Created by bitbucket user evolutics on 2013-08-09 14:35
Last updated on 2016-02-25 16:58

In the attached program, the SIL type checker does not complain about the types in the axiom takeSuccessorCons. This axiom is

  forall x: Natural, y: Natural, ys: List[A] ::
    take(successor(x), cons(y, ys)) == cons(y, take(x, ys))

The type of y should be the abstract type A instead of Natural, since the function cons has the type (A, List[A]): List[A].

Credit goes to Malte for finding this mistake in my axioms!

Attachments:

• undeclared_type_var.sil
• Type_checking_domain.sil

Pull request 🔀 created by bitbucket user severinh on 2014-01-07 16:31
Last updated on 2014-01-07 16:58
Original Bitbucket pull request id: 17

Participants:

• @mschwerhoff (reviewer) ✔️

Source: df41826 on branch severinh/sil/default
Destination: 96236a5 on branch master

State: MERGED

Thank you for letting me know about the 'exhaustiveness' compiler warning. There was indeed a bug in a method that did not have a corresponding unit test.

Created by @alexanderjsummers on 2013-09-01 22:29
Last updated on 2013-11-19 17:02

The attached input file (an attempt to convert Uri's .chalice file) causes a crash when parsing. I don't know whether or not the file in valid SIL. A stack trace is also attached, but it is not very informative (at least, to me)

Attachments:

• AVLTree.iterative.sil
• errors.txt

Pull request 🔀 created by bitbucket user evolutics on 2013-05-25 19:14
Last updated on 2013-05-27 14:48
Original Bitbucket pull request id: 5

Source: unknown commit on branch default of an unknown repo
Destination: 5689766 on branch master
Marge commit: 38264d4

State: MERGED

More transformations I apply when doing the induction translation.

• Transformation of arbitrary program nodes with a partial function. The usage of asInstanceOf seems inevitable here.
• Transformation of specifications in a program tree.

Hopefully, I am using Scala's generics correctly. Please comment if you know a better way to do all this. Thanks.

Created by @mschwerhoff on 2013-07-24 16:42
Last updated on 2013-11-19 16:38

The program

var next: Ref

method foo(this: Ref)
  requires acc(this.next.next, wildcard)
{}

makes the parser fail with

Parse error: Failure: '(' expected but ',' found

Removing the second .next makes the program getting parsed.

Created by @mschwerhoff on 2013-05-29 08:54
Last updated on 2013-11-20 13:11

Multiplying permissions with an integer doesn't seen to work. Expressions such as

exhale acc(this.f, 3 * write)
exhale acc(this.f, 3 * epsilon)

result in the error message expected Perm, but got Int.

Tests can be found in Sil:all/basic/permissions_epsilons.sil.

Created by @alexanderjsummers on 2013-09-04 18:13
Last updated on 2017-11-26 13:36

When nesting acc(..) inside a quantifier, a requirement failure occurs, saying the body of the quantifier can only occur in positive positions. This is confusing, since this is a positive position, plus it is not the whole body which causes the problem. For example:

requires forall x:Int :: (x + 1 > 4 ==> x > 3) && acc(this.f,write)
(not so obvious that the quantifier spans the conjunction, perhaps)

yields "(x + 1 > 4 ==> x > 3) && acc(this.f,write) can only occur in positive positions".

This is also an exception - it would be better to catch this in the resolver/type-checker

Attachments:

• 0025.sil

Created by @alexanderjsummers on 2013-09-04 17:14
Last updated on 2014-05-08 12:58

Omitting the receiver for a field access e.g., this.f causes an "Internal error : variable f is not defined". This should be caught by the type-checker/resolver.

Attachments:

• 0024.sil