Search results

Non-strongly pure condition permitted for If stmt

bugSomething isn't workingSomething isn't working

type checking

Status: Open.

#969 In viperproject/gobra;

· ArquintL opened on Sep 17, 2025

Incompleteness in proving equality of strings

Status: Open.

#966 In viperproject/gobra;

· jcp19 opened on Aug 29, 2025

<code>fix-846</code>: An imported non-<code>ghost</code> <code>hyper</code> function is not considered <code>hyper</code>

Status: Open.

#965 In viperproject/gobra;

· henriman opened on Aug 20, 2025

<code>fix-846</code>: Need relational operator to refer to value in specific program execution

Status: Open.

#963 In viperproject/gobra;

· henriman opened on Aug 18, 2025

<code>fix-846</code>: Gobra crashes when trying to return the value of a field from a <code>hyper</code> function

error reporting

Status: Open.

#962 In viperproject/gobra;

· henriman opened on Aug 18, 2025

Gobra crashes when defining an interface with a predicate and embedding another interface without that predicate

Status: Open.

#959 In viperproject/gobra;

· henriman opened on Aug 13, 2025

Gobra crashes on ghost comparison of interface instances where one interface embeds the other

Status: Open.

#958 In viperproject/gobra;

· henriman opened on Aug 13, 2025

Example of unstable verification (with <code>--hyperMode=on</code>)

Status: Open.

#957 In viperproject/gobra;

· henriman opened on Aug 13, 2025

Neat trick for mutual recursion impossible

Status: Open.

#956 In viperproject/gobra;

· ArquintL opened on Aug 10, 2025

<code>fix-846</code>: Viper encoding leads to insufficient permissions with interfaces

highpriority

Status: Open.

#955 In viperproject/gobra;

· henriman opened on Aug 8, 2025

(hyper)Gobra crashes when implementing interface containing a terminating function (<code>decreases</code>) with a predicate containing <code>low(...)</code> (<code>--hyperMode=on</code>)

SIF

Status: Open.

#949 In viperproject/gobra;

· henriman opened on Jul 25, 2025

<code>decreases</code> in interface introduces non-low branch condition (<code>--hyperMode=on</code>)

SIF

Status: Open.

#948 In viperproject/gobra;

· henriman opened on Jul 18, 2025