viperproject / viperproject/silver

Let expressions inside magic wands cause verifiers to crash

Open
#233 2 comments 0 reactions 1 assignee View on GitHub

@mschwerhoff is already working on this.

Since Feb 20, 2020.

blocker bug
Dominant language
Scala
Stars
100
Forks
53
Avg merge
8h 10m
Merged PRs (30d)
2

Description

Created by @vakaras on 2018-03-18 19:38
Last updated on 2018-03-19 12:54

Example:

#!silver
method test()
    ensures (
        true
        --*
        let tmp2 == (
            true
            ) in (
            tmp2
            --*
            true
        )
    )
{
}

Since this example crashes both back-ends with NoSuchElementException: key not found: tmp2, I suspect that this is a Silver issue. This is a blocking issue for Prusti.

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.