Leave the string replace function undefined for count < 0

runtimeverification · Jan 18, 2024 · 78a51e0 · 78a51e0
1 parent a2393f1
commit 78a51e0
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md
@@ -1885,7 +1885,8 @@ of the above operations in K.
        substrString(Source, 0, findString(Source, ToReplace, 0)) +String Replacement +String
        replace(substrString(Source, findString(Source, ToReplace, 0) +Int lengthString(ToReplace), lengthString(Source)), ToReplace, Replacement, Count -Int 1)
         requires Count >Int 0 andBool findString(Source, ToReplace, 0) >=Int 0
-  rule replace(Source:String, _, _, _) => Source [owise]
+  rule replace(Source:String, _, _, Count) => Source
+        requires Count >= 0 [owise]
   rule replaceAll(Source:String, ToReplace:String, Replacement:String) => replace(Source, ToReplace, Replacement, countAllOccurrences(Source, ToReplace))
 
 endmodule