Completed thesis code

1.1.0

Fix frama-c vnc redirect

Fully proved MinHeap

$ frama-c -rte -wp -wp-prover alt-ergo,cvc4 -wp-par 8 -wp-cache none -wp-timeout 30 -wp-smoke-tests -wp-smoke-timeout 30 src/min_heap.c
[kernel] Parsing src/min_heap.c (with preprocessing)
[kernel] src/min_heap.c:8: Warning:
found two contracts (old location: FRAMAC_SHARE/libc/math.h:1389). Merging them
[kernel] src/min_heap.c:13: Warning:
found two contracts (old location: FRAMAC_SHARE/libc/math.h:1338). Merging them
[rte] annotating function HeapBubbleDown
[rte] annotating function HeapBubbleUp
[rte] annotating function HeapBuild
[rte] annotating function HeapChange
[rte] annotating function HeapDecrease
[rte] annotating function HeapElementValue
[rte] annotating function HeapExternalNodeCount
[rte] annotating function HeapExtractMin
[rte] annotating function HeapFindMin
[rte] annotating function HeapHasBothChildren
[rte] annotating function HeapHasChild
[rte] annotating function HeapHasLeftChild
[rte] annotating function HeapHasParent
[rte] annotating function HeapHasRightChild
[rte] annotating function HeapIncrease
[rte] annotating function HeapInsert
[rte] annotating function HeapInternalNodeCount
[rte] annotating function HeapLeftChild
[rte] annotating function HeapLowerChild
[rte] annotating function HeapParent
[rte] annotating function HeapRightChild
[rte] annotating function HeapSwap
[rte] annotating function _HeapElementValue
[rte] annotating function swapHeapElements
[rte] annotating function swapi
[wp] 484 goals scheduled
[wp] Proved goals: 484 / 484
Qed: 203 (0.30ms-8ms-121ms)
Alt-Ergo 2.2.0: 243 (20ms-30s) (9312) (failed: 2)
CVC4 1.7: 182 (30ms-9.1s-30s) (957095)

MinHeap - FindMin proved