Yushuo Xiao

Wrong 'Content-Length' in response?

6

I am not entirely sure this problem really exists, but I have found that the response for `textDocument/completion` seems to give a wrong `Content-Length`. However, using `racket-langserver` with VSCode is...

I'm interested in your project and want to try out. I have successfully installed the Docker image, built the project, and I am able to run the Maybe example in...

add 多维差分

2

- 希望添加的是什么？ 多维差分（二维及以上） - 英文叫什么？ multi-dimensional difference array - 有什么参考资料？ 基础的内容有很多参考资料； 差分与树状数组合用能够发挥更大作用：参见 @Rabbit-Hu 的博客 [“高级”数据结构——树状数组！](https://www.cnblogs.com/RabbitHu/p/BIT.html)。

Related to #568. The same bug occurs in fold statements as well. ``` field f: Int predicate P(x: Ref, p: Perm) { acc(x.f) } method foo(x: Ref) requires acc(x.f) {...

Incorrect encoding when the predicate argument in an unfold statement contains a permission introspection of the same predicate

1

The following program demonstrates the bug. ``` predicate P(x: Perm) { x == none ==> false } method foo() { inhale P(write) unfold P(perm(P(write))) assert false // successfully verified }...

The known-folded permission mask of a predicate location stores an underestimation of heap locations folded inside the predicate location. The mask is apparently updated during a fold statement, where heap...

In the Viper program below, predicate `P` contains zero permission to `x.f`. When `fold P(x)` updates the known-folded permission mask of `P`, `x.f` is added without checking if the permission...

Fixing issue #572. However, one test case [all/issues/silicon/0113.vpr](https://github.com/viperproject/silver/blob/b09d0791cb2b2683947190645aefd20f4f54dacf/src/test/resources/all/issues/silicon/0113.vpr) does not pass. Problem has not been identified yet.

Since we now check the permission amount for strict positivity in fold statements, it is unnecessary to check if the state has zero direct permission to the predicate instance afterwards...

Test case sensitive to Z3 seeds

1

The following test case is very sensitive to Z3 seeds and may cause non-termination. - [`all/functions/linkedlists.vpr`](https://github.com/viperproject/silver/blob/63c30b18fdafd81d90eabbc8bccfd13a31becd61/src/test/resources/all/functions/linkedlists.vpr)