File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -1231,3 +1231,17 @@ def is_valid_mem(self) -> bool:
12311231
12321232 def __str__ (self ) -> str :
12331233 return "valid-mem(" + str (self .term ) + ")"
1234+
1235+
1236+ @ifdregistry .register_tag ("ew" , XPredicate )
1237+ class XWritesErrno (XPredicate ):
1238+ """errno must have been written locally.
1239+ """
1240+
1241+ def __init__ (
1242+ self , ifd : "InterfaceDictionary" , ixval : IT .IndexedTableValue
1243+ ) -> None :
1244+ XPredicate .__init__ (self , ifd , ixval )
1245+
1246+ def __str__ (self ) -> str :
1247+ return "errno-must-written()"
Original file line number Diff line number Diff line change @@ -2231,6 +2231,7 @@ def is_preserves_all_memory(self) -> bool:
22312231 def __str__ (self ) -> str :
22322232 return "preserves-all-memory()"
22332233
2234+
22342235@pdregistry .register_tag ("ew" , CPOPredicate )
22352236class CPOErrnoMustBeWritten (CPOPredicate ):
22362237 """errno-must-written(): true if errno must have been written locally.
@@ -2248,6 +2249,7 @@ def is_errno_must_written(self) -> bool:
22482249 def __str__ (self ) -> str :
22492250 return "errno-must-written()"
22502251
2252+
22512253@pdregistry .register_tag ("pv" , CPOPredicate )
22522254class CPOPreservedValue (CPOPredicate ):
22532255 """preserves-value(exp): true of a function that preserves the value of exp.
You can’t perform that action at this time.
0 commit comments