fix errors

router/dataplane.go

@@ -188,15 +188,17 @@ type scmpError struct {
 	Cause    error
 }
 
+// Gobra cannot currently prove termination of this function,
+// because it is not specified how the ErrorMem() of the result
+// of serrors.New relates to that of e.
+// @ trusted
 // @ preserves e.ErrorMem()
-// @ decreases e.Size()
+// @ ensures   e.IsDuplicableMem() == old(e.IsDuplicableMem())
+// @ decreases e.ErrorMem()
 func (e scmpError) Error() string {
 	// @ unfold e.ErrorMem()
 	// @ defer fold e.ErrorMem()
-	res := serrors.New("scmp", "typecode", e.TypeCode, "cause", e.Cause)
-	// TODO: doc
-	// @ assume res.Size() == 1 + e.Cause.Size()
-	return res.Error()
+	return serrors.New("scmp", "typecode", e.TypeCode, "cause", e.Cause).Error()
 }
 
 // SetIA sets the local IA for the dataplane.

router/dataplane_spec.gobra

@@ -153,18 +153,26 @@ pred (err scmpError) ErrorMem() {
 }
 
 ghost
-pure
+// Gobra currently runs into unexpected verification errors
+// when trying to prove the termination of this function.
+// (https://github.com/viperproject/gobra/issues/702)
+trusted
 requires  acc(err.ErrorMem(), _)
-decreases err.Size()
-func (err scmpError) IsDuplicableMem() bool {
+decreases err.ErrorMem()
+pure func (err scmpError) IsDuplicableMem() bool {
 	return unfolding acc(err.ErrorMem(), _) in
 		err.Cause.IsDuplicableMem()
 }
 
 ghost
+// Gobra currently runs into unexpected verification errors
+// when trying to prove the termination of this function.
+// (https://github.com/viperproject/gobra/issues/702)
+trusted
 preserves err.ErrorMem()
+ensures   err.IsDuplicableMem() == old(err.IsDuplicableMem())
 ensures   err.IsDuplicableMem() ==> err.ErrorMem()
-decreases err.Size()
+decreases err.ErrorMem()
 func (err scmpError) Duplicate() {
 	if err.IsDuplicableMem() {
 		unfold err.ErrorMem()
@@ -176,15 +184,6 @@ func (err scmpError) Duplicate() {
 	}
 }
 
-ghost
-requires acc(e.ErrorMem(), _)
-ensures  0 < res
-pure func (e scmpError) Size() (res int) {
-	return unfolding acc(e.ErrorMem(), _) in
-		let _ := Asserting(0 <= e.Cause.Size()) in
-		2 + e.Cause.Size()
-}
-
 scmpError implements error
 
 type offsetPair struct {

verification/dependencies/syscall/syscall_unix.gobra

@@ -28,6 +28,7 @@ Errno implements error
 pred (e Errno) ErrorMem() { e != 0 }
 
 preserves e.ErrorMem()
+ensures   old(e.IsDuplicableMem()) == e.IsDuplicableMem()
 decreases
 func (e Errno) Error() string
 
@@ -41,19 +42,13 @@ func (e Errno) IsDuplicableMem() (res bool) {
 ghost
 preserves e.ErrorMem()
 ensures   e.ErrorMem()
+ensures   old(e.IsDuplicableMem()) == e.IsDuplicableMem()
 decreases
 func (e Errno) Duplicate() {
 	assert unfolding e.ErrorMem() in true
 	fold e.ErrorMem()
 }
 
-ghost
-requires acc(e.ErrorMem(), _)
-ensures  0 <= res
-pure func (e Errno) Size() (res int) {
-	return 0
-}
-
 /** ErrorCell **/
 pred (s *Errno) Mem() {
 	acc(s)