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

[fanweneddie]

Hi there,

I am wondering what the test case in c0 file looks like for Daisy's example of swapping the branches of predicate acyclicSeg() in paper GC0-24 (shown below).

predicate acyclicSeg(struct Node *from, struct Node *to) =
    (from == to) ?
        (acc(from->val) && acc(from->next) && acyclicSeg(from->next, to))
        :
        (true)
        ;

For this example, section 3.2 in the paper states that Viper requires 3 increments to help Daisy detect the bug, while gc0 only requires Daisy to provide 1 increment, a ? on the loop invariant and a simple test case that calls insertLast() on a list with one node. However, I don't know what the test case looks like, and listInsertGradualFeedback1.c0 is what I guess.

The c0 file above contains function createList() to create a list and function calls list = createList(3); list = insertLast(list, 1); in main() function as a simple testcase. (By the way, I think I have to fully specify function createList(), otherwise the list for insertLast() cannot satisfy the precondition of acyclic(list).) Moreover, this file only specifies the first increment in insertLast() and leaves the loop invariant as ?. I am not sure whether it fits the description of section 3.2 of the paper. On gvc0, this feedback is given:

sbt:gvc0> run src/test/resources/quant-study/listInsertGradualFeedback1.c0
[info] running (fork) gvc.Main src/test/resources/quant-study/listInsertGradualFeedback1.c0
[info] [*] — Mon Jun 17 15:51:15 GMT 2024
[error] Exception in thread "main" gvc.VerificationException: Folding acyclicSeg(newHead.Node$next, null) might fail. There might be insufficient permission to access from.Node$val. (<no position>)

which may fit this description in the paper ("reporting at run time that acc(s->val) from acyclicSeg does not hold at the end of the list where s == NULL").

I am wondering whether the testcase in the c0 file that I provide fits the paper or not. Thanks for your time.