Apply suggestions from code review

viperproject · Dec 2, 2024 · b8eefef · b8eefef
1 parent 70bb22d
commit b8eefef
Show file tree

Hide file tree

Showing 6 changed files with 0 additions and 20 deletions.
diff --git a/pkg/slayers/path/epic/epic_spec.gobra b/pkg/slayers/path/epic/epic_spec.gobra
@@ -74,8 +74,6 @@ pure func (p *Path) getPHVFLen(buf []byte) (l int) {
 
 ghost
 requires acc(p.Mem(buf), _)
-// TODO: drop post
-ensures l == (unfolding acc(p.Mem(buf), _) in len(p.LHVF))
 decreases
 pure func (p *Path) getLHVFLen(buf []byte) (l int) {
 	return unfolding acc(p.Mem(buf), _) in len(p.LHVF)

diff --git a/pkg/slayers/path/path_spec.gobra b/pkg/slayers/path/path_spec.gobra
@@ -67,8 +67,6 @@ pred PathPackageMem() {
 ghost
 requires 0 <= t && t < maxPathType
 requires acc(PathPackageMem(), _)
-// TODO: drop post
-ensures  res == unfolding acc(PathPackageMem(), _) in registeredPaths[t].inUse
 decreases
 pure func Registered(t Type) (res bool) {
 	return unfolding acc(PathPackageMem(), _) in registeredPaths[t].inUse

diff --git a/pkg/slayers/path/scion/decoded_spec.gobra b/pkg/slayers/path/scion/decoded_spec.gobra
@@ -66,8 +66,6 @@ func (d *Decoded) Len(ghost ubuf []byte) (l int) {
 
 ghost
 requires acc(d.Mem(ub), _)
-// TODO: drop post
-ensures  unfolding acc(d.Mem(ub), _) in l == d.Base.Len()
 decreases
 pure func (d *Decoded) LenSpec(ghost ub []byte) (l int) {
 	return unfolding acc(d.Mem(ub), _) in d.Base.Len()
@@ -80,8 +78,6 @@ pure func (d *Decoded) LenSpec(ghost ub []byte) (l int) {
   * introduced this method which acts as a wrapper.
   */
 requires acc(d.Mem(ubuf), _)
-// TODO: drop post
-ensures  unfolding acc(d.Mem(ubuf), _) in t == d.Base.Type()
 decreases
 pure func (d *Decoded) Type(ghost ubuf []byte) (t path.Type) {
 	return unfolding acc(d.Mem(ubuf), _) in d.Base.Type()

diff --git a/pkg/slayers/path/scion/raw_spec.gobra b/pkg/slayers/path/scion/raw_spec.gobra
@@ -59,8 +59,6 @@ pure func (s *Raw) IsValidResultOfDecoding(buf []byte, err error) (res bool) {
   * introduced this wrapper method which acts as a wrapper.
   */
 requires acc(s.Mem(buf), _)
-// TODO: drop post
-ensures  unfolding acc(s.Mem(buf), _) in t == s.Base.Type()
 decreases
 pure func (s *Raw) Type(ghost buf []byte) (t path.Type) {
 	return unfolding acc(s.Mem(buf), _) in s.Base.Type()
@@ -81,8 +79,6 @@ func (s *Raw) Len(ghost buf []byte) (l int) {
 
 ghost
 requires acc(s.Mem(ub), _)
-// TODO: drop post
-ensures  unfolding acc(s.Mem(ub), _) in l == s.Base.Len()
 decreases
 pure func (s *Raw) LenSpec(ghost ub []byte) (l int) {
 	return unfolding acc(s.Mem(ub), _) in s.Base.Len()

diff --git a/verification/dependencies/github.com/google/gopacket/layertype.gobra b/verification/dependencies/github.com/google/gopacket/layertype.gobra
@@ -49,8 +49,6 @@ pred LayerTypesMem() {
 
 ghost
 requires acc(LayerTypesMem(), _)
-// TODO: drop post
-ensures  res == unfolding acc(LayerTypesMem(), _) in (0 <= t && t < MaxLayerType? ltMeta[t].inUse : (t in domain(ltMetaMap) && ltMetaMap[t].inUse))
 decreases
 pure func Registered(t LayerType) (res bool) {
 	return unfolding acc(LayerTypesMem(), _) in
@@ -59,8 +57,6 @@ pure func Registered(t LayerType) (res bool) {
 
 ghost
 requires acc(&ltMeta, _) && acc(&ltMetaMap, _) && acc(ltMetaMap, _) && acc(&DecodersByLayerName, _) && acc(DecodersByLayerName, _)
-// TODO: drop post
-ensures  res == (0 <= t && t < MaxLayerType? ltMeta[t].inUse : (t in domain(ltMetaMap) && ltMetaMap[t].inUse))
 decreases
 pure func registeredDuringInit(t LayerType) (res bool) {
 	return (0 <= t && t < MaxLayerType? ltMeta[t].inUse : (t in domain(ltMetaMap) && ltMetaMap[t].inUse))

diff --git a/verification/dependencies/strings/strings.gobra b/verification/dependencies/strings/strings.gobra
@@ -95,16 +95,12 @@ decreases _
 pure func Join(elems []string, sep string) (res string)
 
 // HasPrefix tests whether the string s begins with prefix.
-// TODO: drop post
-ensures ret == (len(s) >= len(prefix) && s[0:len(prefix)] == prefix)
 decreases
 pure func HasPrefix(s, prefix string) (ret bool) {
 	return len(s) >= len(prefix) && (s[0:len(prefix)] == prefix)
 }
 
 // HasSuffix tests whether the string s ends with suffix.
-// TODO: drop post
-ensures ret == (len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix)
 decreases
 pure func HasSuffix(s, suffix string) (ret bool) {
 	return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix