From 9240c0dcbd5ca097d34355bfa75d8cdb998534bc Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Thu, 13 Aug 2026 22:28:04 +0400 Subject: [PATCH 1/2] adjust one test to use derive_constraints command --- src/exercises/queue/push_induction.c | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/exercises/queue/push_induction.c b/src/exercises/queue/push_induction.c index 37b2ad34..62d80851 100644 --- a/src/exercises/queue/push_induction.c +++ b/src/exercises/queue/push_induction.c @@ -19,9 +19,11 @@ void push_induction(struct queue_cell* front @*/ { if (front == second_last) { + /*@ derive_constraints(RW(second_last), RW(last)); @*/ /*@ unfold Snoc(Q, Second_last.first); @*/ return; } else { + /*@ derive_constraints(RW(front), RW(second_last), RW(last)); @*/ push_induction(front->next, second_last, last); /*@ unfold Snoc(Q, Second_last.first); @*/ return; From 88681970e0b0ad153447e4f52e0d6d18005f595d Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Tue, 18 Aug 2026 12:54:54 +0100 Subject: [PATCH 2/2] fix two tests wrt CN changes --- src/example-archive/simple-examples/working/power_1.c | 2 ++ src/example-archive/simple-examples/working/power_2.c | 3 +++ 2 files changed, 5 insertions(+) diff --git a/src/example-archive/simple-examples/working/power_1.c b/src/example-archive/simple-examples/working/power_1.c index cf84ca21..e76feba5 100644 --- a/src/example-archive/simple-examples/working/power_1.c +++ b/src/example-archive/simple-examples/working/power_1.c @@ -7,6 +7,8 @@ // 1. the base case - power_uf(2,0) = 1 // 2. the inductive case - power(2,y+1) == 2 * power_uf(2,y) +/*@ function (i32) power_uf(i32 x, i32 y) @*/ + void lemma_power_uf_def(int y) /*@ trusted; requires y >= 0i32; diff --git a/src/example-archive/simple-examples/working/power_2.c b/src/example-archive/simple-examples/working/power_2.c index caf3e1d1..3d7d3444 100644 --- a/src/example-archive/simple-examples/working/power_2.c +++ b/src/example-archive/simple-examples/working/power_2.c @@ -1,5 +1,8 @@ // Compute 2^1 +/*@ function (i32) power_uf(i32 x, i32 y) @*/ + + /*@ lemma LemmaPowerUFDef(i32 y) requires