Skip to content

Commit 1639ab5

Browse files
committed
Add executable models of CProverString functions
These models can be compiled and run and have the same semantics as implemented by the string solver. They can thus be used to check that the string solver gives the correct result by comparing the result of a concrete run with the result obtained by cbmc.
1 parent 1a9435a commit 1639ab5

File tree

2 files changed

+8
-0
lines changed

2 files changed

+8
-0
lines changed
Binary file not shown.

jbmc/regression/jbmc-strings/cprover/CProverString.java

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -147,4 +147,12 @@ public static StringBuffer insert(
147147
StringBuffer sb, int offset, long l) {
148148
return sb.insert(offset, l);
149149
}
150+
151+
public static String toString(int i) { return String.valueOf(i); }
152+
153+
public static String toString(long l) { return String.valueOf(l); }
154+
155+
public static String toString(float f) { return String.valueOf(f); }
156+
157+
public static String toString(double d) { return String.valueOf((float)d); }
150158
}

0 commit comments

Comments
 (0)