THE Release

1.0.0

cleanup

ghost param in function -- contiki wrong

Its really memory/time problem for SMT - separation and reachability

// length(head) < 3, timeout 5 -> ok
// length(head) < 4, timout 5 -> not ok
// length(head) < 4, timout 10 -> ok
// length(head) < 5 -> not ok

NOT!! found separation example, that does not break head

contradiction??

node and &node->next cant be separated

F-c OK - the problem seems to be the difference when new_head is modeled using Hoare mem model and when memory is taken (for example assert finite(&new_head);) it switches to different mode

F-c writing to null varaible in struct can be proven correct, otherwise not?

---

F-c WHAT? local variable breaks finitenes??

po odstraneni int fieldu z lisu

---

Guide to Software Verification with Frama-C > 4.3 + 4.3.8

AVL delete

0.0.4

delete verified

AVL insert

0.0.3

insert verified

AVL rotations

0.0.2

proved all 4 rotations