Search results

Bug in Runtime Check Generation

Status: Open.

#70 In gradual-verification/gvc0;

· thanhlecongg opened on Apr 30, 2025

Question about the testcase in the c0 file for Daisy's first example in the paper

Status: Open.

#65 In gradual-verification/gvc0;

· fanweneddie opened on Jun 17, 2024

Lemmas functions should become a specification construct + be removed from programs when completely statically verified

enhancementNew feature or requestNew feature or request

questionFurther information is requestedFurther information is requested

Status: Open.

#63 In gradual-verification/gvc0;

· jennalwise opened on Jun 9, 2024

Benchmarker producing wrong .verified files after generating correct source code permutations due to oddly constructed IRs

enhancementNew feature or requestNew feature or request

Status: Open.

#59 In gradual-verification/gvc0;

· jennalwise opened on Nov 15, 2023

Need to catch logical conditionals with impure conditions in frontend and produce error message

bugSomething isn't workingSomething isn't working

enhancementNew feature or requestNew feature or request

Status: Open.

#57 In gradual-verification/gvc0;

· jennalwise opened on Sep 28, 2023

Run-time checks with char comparison should use char val not int val

bugSomething isn't workingSomething isn't working

Status: Open.

#56 In gradual-verification/gvc0;

· jennalwise opened on Sep 26, 2023

Permutation generator does not support treating missing <code>requires</code> and <code>ensures</code> specifications as <code>true</code>

Status: Open.

#53 In gradual-verification/gvc0;

· icmccorm opened on Aug 1, 2023

Verifier is unsound for bad specs involving method calls with equi-imprecise preconditions; discussion in Conrad's paper

enhancementNew feature or requestNew feature or request

Status: Open.

#52 In gradual-verification/gvc0;

· jennalwise opened on Jul 28, 2023

Recursive predicates should fail due to separation rather than infinite recursion if separation failure applies

enhancementNew feature or requestNew feature or request

Status: Open.

#49 In gradual-verification/gvc0;

· jennalwise opened on Apr 21, 2023

line numbers for static errors

enhancementNew feature or requestNew feature or request

Status: Open.

#48 In gradual-verification/gvc0;

· JonathanAldrich opened on Apr 18, 2023

Invalid acc() argument exception

Status: Open.

#47 In gradual-verification/gvc0;

· JonathanAldrich opened on Apr 11, 2023

"Invalid specification" is an overly general &amp; unhelpful error message

Status: Open.

#46 In gradual-verification/gvc0;

· JonathanAldrich opened on Apr 11, 2023