Changes to avoid unnecessary assumptions (#246)

* try out a few changes * continue * continue * backup * fix preds * backup * continue * continue efforts * last setter * fix perm for runningPerm * only Run missing now * backup * cleanup unnecessary symbols * store progress * backup current status * backup * backup * backup * backup * backup * rm file commited by mistake * backup * backup * fix calls to initMetrics * backup * further cleanup * fix verification error
viperproject · Feb 19, 2024 · e71ba3a · e71ba3a
1 parent 685c562
commit e71ba3a
Show file tree

Hide file tree

Showing 5 changed files with 580 additions and 387 deletions.
diff --git a/router/assumptions.gobra b/router/assumptions.gobra
@@ -39,6 +39,12 @@ ensures malformedPath.ErrorMem()
 decreases _
 func establishMemMalformedPath()
 
+ghost
+ensures alreadySet != nil
+ensures alreadySet.ErrorMem()
+decreases _
+func establishAlreadySet()
+
 ghost
 ensures unsupportedPathTypeNextHeader.ErrorMem()
 decreases _