Regressions tests for string functions
This commit is contained in:
parent
f5493d781c
commit
e6d97e1a3b
|
@ -0,0 +1,3 @@
|
|||
|
||||
test:
|
||||
../test.pl -c ../../../src/cbmc/cbmc
|
|
@ -0,0 +1,73 @@
|
|||
typedef struct __CPROVER_string { char *s; } __CPROVER_string;
|
||||
//typedef struct __CPROVER_char { char c; } __CPROVER_char;
|
||||
typedef unsigned char __CPROVER_char;
|
||||
|
||||
/******************************************************************************
|
||||
* CPROVER string functions
|
||||
******************************************************************************/
|
||||
/* returns s[p] */
|
||||
#define __CPROVER_char_at(s, p) __CPROVER_uninterpreted_string_char_at_func(s, p)
|
||||
|
||||
/* string equality */
|
||||
#define __CPROVER_string_equal(s1, s2) __CPROVER_uninterpreted_string_equal_func(s1, s2)
|
||||
|
||||
/* defines a string literal, e.g. __CPROVER_string_literal("foo") */
|
||||
#define __CPROVER_string_literal(s) __CPROVER_uninterpreted_string_literal_func(s)
|
||||
|
||||
/* defines a char literal, e.g. __CPROVER_char_literal("c"). NOTE: you
|
||||
* *must* use a C string literal as argument (i.e. double quotes "c", not
|
||||
* single 'c') */
|
||||
#define __CPROVER_char_literal(c) __CPROVER_uninterpreted_char_literal_func(c)
|
||||
|
||||
/* produces the concatenation of s1 and s2 */
|
||||
#define __CPROVER_string_concat(s1, s2) __CPROVER_uninterpreted_string_concat_func(s1, s2)
|
||||
|
||||
/* return the length of s */
|
||||
#define __CPROVER_string_length(s) __CPROVER_uninterpreted_string_length_func(s)
|
||||
|
||||
/* extracts the substring between positions i and j (j not included) */
|
||||
#define __CPROVER_string_substring(s, i, j) __CPROVER_uninterpreted_string_substring_func(s, i, j)
|
||||
|
||||
/* test whether p is a prefix of s */
|
||||
#define __CPROVER_string_isprefix(p, s) __CPROVER_uninterpreted_string_is_prefix_func(p, s)
|
||||
|
||||
/* test whether p is a suffix of s */
|
||||
#define __CPROVER_string_issuffix(p, s) __CPROVER_uninterpreted_string_is_suffix_func(p, s)
|
||||
/* test whether p contains s */
|
||||
#define __CPROVER_string_contains(p, s) __CPROVER_uninterpreted_string_contains_func(p, s)
|
||||
|
||||
/* first index where character c appears, -1 if not found */
|
||||
#define __CPROVER_string_index_of(s, c) __CPROVER_uninterpreted_string_index_of_func(s, c)
|
||||
|
||||
/* last index where character c appears */
|
||||
#define __CPROVER_string_last_index_of(s, c) __CPROVER_uninterpreted_string_last_index_of_func(s, c)
|
||||
|
||||
/* returns a new string obtained from s by setting s[p] = c */
|
||||
#define __CPROVER_char_set(s, p, c) __CPROVER_uninterpreted_string_char_set_func(s, p, c)
|
||||
|
||||
|
||||
#define __CPROVER_string_copy(s) __CPROVER_uninterpreted_string_copy_func(s)
|
||||
#define __CPROVER_parse_int(s) __CPROVER_uninterpreted_string_parse_int_func(s)
|
||||
#define __CPROVER_string_of_int(i) __CPROVER_uninterpreted_string_of_int_func(i)
|
||||
|
||||
|
||||
/******************************************************************************
|
||||
* don't use these directly
|
||||
******************************************************************************/
|
||||
extern __CPROVER_char __CPROVER_uninterpreted_string_char_at_func(__CPROVER_string str, int pos);
|
||||
extern __CPROVER_bool __CPROVER_uninterpreted_string_equal_func(__CPROVER_string str1, __CPROVER_string str2);
|
||||
extern __CPROVER_string __CPROVER_uninterpreted_string_literal_func();
|
||||
extern __CPROVER_char __CPROVER_uninterpreted_char_literal_func();
|
||||
extern __CPROVER_string __CPROVER_uninterpreted_string_concat_func(__CPROVER_string str1, __CPROVER_string str2);
|
||||
extern int __CPROVER_uninterpreted_string_length_func(__CPROVER_string str);
|
||||
extern __CPROVER_string __CPROVER_uninterpreted_string_substring_func(__CPROVER_string str, int i, int j);
|
||||
extern __CPROVER_bool __CPROVER_uninterpreted_string_is_prefix_func(__CPROVER_string pref, __CPROVER_string str);
|
||||
extern __CPROVER_bool __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_string suff, __CPROVER_string str);
|
||||
extern __CPROVER_bool __CPROVER_uninterpreted_string_contains_func(__CPROVER_string str1, __CPROVER_string str2);
|
||||
extern int __CPROVER_uninterpreted_string_index_of_func(__CPROVER_string str, __CPROVER_char c);
|
||||
extern int __CPROVER_uninterpreted_string_last_index_of_func(__CPROVER_string str, __CPROVER_char c);
|
||||
extern __CPROVER_string __CPROVER_uninterpreted_string_char_set_func(__CPROVER_string str, int pos, __CPROVER_char c);
|
||||
extern __CPROVER_string __CPROVER_uninterpreted_string_copy_func(__CPROVER_string str);
|
||||
extern unsigned __CPROVER_uninterpreted_string_parse_int_func(__CPROVER_string str);
|
||||
extern __CPROVER_string __CPROVER_uninterpreted_string_of_int_func(unsigned i);
|
||||
|
|
@ -0,0 +1,10 @@
|
|||
CORE
|
||||
test_case.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_case.java line 11: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_case.java line 12: SUCCESS$
|
||||
^\[assertion.3\] assertion at file test_case.java line 13: SUCCESS$
|
||||
^\[assertion.4\] assertion at file test_case.java line 14: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,16 @@
|
|||
public class test_case {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
|
||||
String s = new String("AbcCdE");
|
||||
String l = s.toLowerCase();
|
||||
System.out.println(l);
|
||||
|
||||
String u = s.toUpperCase();
|
||||
System.out.println(u);
|
||||
assert(l.equals("abccde"));
|
||||
assert(u.equals("ABCCDE"));
|
||||
assert(s.equalsIgnoreCase("ABccDe"));
|
||||
assert(!l.equals("abccde") || !u.equals("ABCCDE"));
|
||||
}
|
||||
}
|
|
@ -0,0 +1,9 @@
|
|||
CORE
|
||||
test_char_at.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_char_at.java line 11: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_char_at.java line 13: FAILURE$
|
||||
^\[assertion.3\] assertion at file test_char_at.java line 15: SUCCESS$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,17 @@
|
|||
public class test_char_at {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
String s = new String("Hello World!");
|
||||
char c = s.charAt(4);
|
||||
StringBuilder sb = new StringBuilder(s);
|
||||
sb.setCharAt(5,'-');
|
||||
s = sb.toString();
|
||||
|
||||
if(argv.length==1)
|
||||
assert(c == 'o');
|
||||
else if(argv.length==2)
|
||||
assert(c == 'p');
|
||||
else
|
||||
assert(s.equals("Hello-World!"));
|
||||
}
|
||||
}
|
|
@ -0,0 +1,11 @@
|
|||
CORE
|
||||
test_code_point.class
|
||||
--pass
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_code_point.java line 5: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_code_point.java line 6: SUCCESS$
|
||||
^\[assertion.3\] assertion at file test_code_point.java line 7: SUCCESS$
|
||||
^\[assertion.4\] assertion at file test_code_point.java line 8: SUCCESS$
|
||||
^\[assertion.5\] assertion at file test_code_point.java line 11: SUCCESS$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,13 @@
|
|||
public class test_code_point {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
String s = "!𐤇𐤄𐤋𐤋𐤅";
|
||||
assert(s.codePointAt(1) == 67847);
|
||||
assert(s.codePointBefore(3) == 67847);
|
||||
assert(s.codePointCount(1,5) >= 2);
|
||||
assert(s.offsetByCodePoints(1,2) >= 3);
|
||||
StringBuilder sb = new StringBuilder();
|
||||
sb.appendCodePoint(0x10907);
|
||||
assert(s.charAt(1) == sb.charAt(0));
|
||||
}
|
||||
}
|
|
@ -0,0 +1,10 @@
|
|||
CORE
|
||||
test_compare.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_compare.java line 6: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_compare.java line 8: FAILURE$
|
||||
^\[assertion.3\] assertion at file test_compare.java line 11: SUCCESS$
|
||||
^\[assertion.4\] assertion at file test_compare.java line 12: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,18 @@
|
|||
public class test_compare {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
String s1 = "abc";
|
||||
String s2 = "aac";
|
||||
assert(s1.compareTo(s2) == 1);
|
||||
|
||||
assert(s2.compareTo(argv[0]) != -1);
|
||||
|
||||
String s3 = "abc";
|
||||
assert(s3.hashCode() == s1.hashCode());
|
||||
assert(s3.hashCode() == s2.hashCode());
|
||||
|
||||
/*String x = s1.intern();
|
||||
String y = s3.intern();
|
||||
assert(x == y);*/
|
||||
}
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
test_concat.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_concat.java line 9: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_concat.java line 10: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,12 @@
|
|||
public class test_concat {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
String s = new String("pi");
|
||||
int i = s.length();
|
||||
String t = new String("ppo");
|
||||
String u = s.concat(t);
|
||||
char c = u.charAt(i);
|
||||
assert(c == 'p');
|
||||
assert(c == 'o');
|
||||
}
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
KNOWNBUG
|
||||
test_contains.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_contains.java line 7: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_contains.java line 8: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,10 @@
|
|||
public class test_contains {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
String s = new String("Hello World!");
|
||||
String u = "o W";
|
||||
String t = "W o";
|
||||
assert(s.contains(u));
|
||||
assert(s.contains(t));
|
||||
}
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
KNOWNBUG
|
||||
test_delete.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_delete.java line 11: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_delete.java line 12: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,15 @@
|
|||
public class test_delete {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
StringBuilder s = new StringBuilder();
|
||||
s.append("Hello World!");
|
||||
s.delete(4,6);
|
||||
s.deleteCharAt(1);
|
||||
|
||||
String str = s.toString();
|
||||
System.out.println(str);
|
||||
assert(str.equals("HllWorld!"));
|
||||
assert(!str.equals("HllWorld!"));
|
||||
|
||||
}
|
||||
}
|
Binary file not shown.
|
@ -0,0 +1,34 @@
|
|||
public class easychair {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
if(argv.length > 1){
|
||||
String str = new String(argv[1]);
|
||||
if(str.length() < 40){
|
||||
|
||||
// containing "/" and containing "EasyChair"
|
||||
int lastSlash = str.lastIndexOf('/');
|
||||
if(lastSlash < 0) return ;
|
||||
|
||||
String rest = str.substring(lastSlash + 1);
|
||||
// warning: removed this because contains is not efficient at the moment
|
||||
if(! rest.contains("EasyChair")) return ;
|
||||
// (2) Check that str starts with "http://"
|
||||
if(! str.startsWith("http://")) return ;
|
||||
// (3) Take the string between "http://" and the last "/".
|
||||
// if it starts with "www." strip the "www." off
|
||||
String t = str.substring("http://".length(),lastSlash - "http://".length());
|
||||
if(t.startsWith("www."))
|
||||
t = t.substring("www.".length());
|
||||
|
||||
//
|
||||
//(4) Check that after stripping we have either "live.com"
|
||||
// or "google.com"
|
||||
if(!t.equals("live.com") && !t.equals("google.com"))
|
||||
return ;
|
||||
// s survived all checks
|
||||
assert(false); //return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
}
|
|
@ -0,0 +1,7 @@
|
|||
KNOWNBUG
|
||||
easychair.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file easychair.java line 29: FAILURE$
|
||||
--
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
test_empty.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_empty.java line 4: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_empty.java line 5: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,7 @@
|
|||
public class test_empty {
|
||||
public static void main(String[] argv) {
|
||||
String empty = " ";
|
||||
assert(empty.trim().isEmpty());
|
||||
assert(empty.isEmpty());
|
||||
}
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
test_equal.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_equal.java line 7: FAILURE$
|
||||
^\[assertion.2\] assertion at file test_equal.java line 8: SUCCESS$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,10 @@
|
|||
public class test_equal {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
String s = new String("pi");
|
||||
String t = new String("po");
|
||||
String u = "po";
|
||||
assert(s.equals(t));
|
||||
assert(t.equals(u));
|
||||
}
|
||||
}
|
|
@ -0,0 +1,10 @@
|
|||
CORE
|
||||
test_float.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_float.java line 14: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_float.java line 15: SUCCESS$
|
||||
^\[assertion.3\] assertion at file test_float.java line 16: SUCCESS$
|
||||
^\[assertion.4\] assertion at file test_float.java line 17: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,20 @@
|
|||
public class test_float {
|
||||
|
||||
public static void main(String[] arg) {
|
||||
float inf = 100.0f / 0.0f;
|
||||
float minus_inf = -100.0f / 0.0f;
|
||||
float nan = 0.0f / 0.0f;
|
||||
String inf_string = Float.toString(inf);
|
||||
String mininf_string = Float.toString(minus_inf);
|
||||
String nan_string = Float.toString(nan);
|
||||
//String arg1 = arg[0];
|
||||
System.out.println(nan_string);
|
||||
System.out.println(inf_string);
|
||||
System.out.println(mininf_string);
|
||||
assert(nan_string.equals("NaN"));
|
||||
assert(inf_string.equals("Infinity"));
|
||||
assert(mininf_string.equals("-Infinity"));
|
||||
assert(!nan_string.equals("NaN") || !inf_string.equals("Infinity")
|
||||
|| !mininf_string.equals("-Infinity"));
|
||||
}
|
||||
}
|
|
@ -0,0 +1,16 @@
|
|||
CORE
|
||||
test_index_of.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_index_of.java line 13: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_index_of.java line 14: FAILURE$
|
||||
^\[assertion.3\] assertion at file test_index_of.java line 17: SUCCESS$
|
||||
^\[assertion.4\] assertion at file test_index_of.java line 18: FAILURE$
|
||||
^\[assertion.5\] assertion at file test_index_of.java line 21: SUCCESS$
|
||||
^\[assertion.6\] assertion at file test_index_of.java line 22: FAILURE$
|
||||
^\[assertion.7\] assertion at file test_index_of.java line 25: SUCCESS$
|
||||
^\[assertion.8\] assertion at file test_index_of.java line 26: FAILURE$
|
||||
^\[assertion.9\] assertion at file test_index_of.java line 28: SUCCESS$
|
||||
^\[assertion.10\] assertion at file test_index_of.java line 29: SUCCESS$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,32 @@
|
|||
public class test_index_of {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
String s = "Hello World!";
|
||||
char c = 'o';
|
||||
int i = s.indexOf(c);
|
||||
int j = s.lastIndexOf('o');
|
||||
int k = s.indexOf(c,5);
|
||||
int l = s.lastIndexOf(c,5);
|
||||
int m = s.indexOf("lo");
|
||||
int n = s.lastIndexOf("lo");
|
||||
if(argv.length == 1){
|
||||
assert(i == 4);
|
||||
assert(i != 4);
|
||||
}
|
||||
else if(argv.length == 2){
|
||||
assert(j == 7);
|
||||
assert(j != 7);
|
||||
}
|
||||
else if(argv.length == 3){
|
||||
assert(k == 7);
|
||||
assert(k != 7);
|
||||
}
|
||||
else if(argv.length == 4){
|
||||
assert(l == 4);
|
||||
assert(l != 4);
|
||||
} else {
|
||||
assert(m != 2);
|
||||
assert(n != 2);
|
||||
}
|
||||
}
|
||||
}
|
Binary file not shown.
|
@ -0,0 +1,19 @@
|
|||
public class test_insert {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
int i = 123;
|
||||
long j = 123;
|
||||
char c = '/';
|
||||
boolean b = true;
|
||||
StringBuilder sb = new StringBuilder("hello");
|
||||
sb.insert(2,i);
|
||||
sb.insert(2,c);
|
||||
sb.insert(2,j);
|
||||
sb.insert(2,b);
|
||||
sb.insert(2,"abc");
|
||||
String s = sb.toString();
|
||||
System.out.println(s);
|
||||
assert(s.equals("heabctrue123/123llo"));
|
||||
assert(!s.equals("heabctrue123/123llo"));
|
||||
}
|
||||
}
|
Binary file not shown.
|
@ -0,0 +1,23 @@
|
|||
public class test_insert1 {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
int i = 123;
|
||||
long j = 123;
|
||||
char c = '/';
|
||||
boolean b = true;
|
||||
StringBuilder sb = new StringBuilder("hello");
|
||||
sb.insert(2,i);
|
||||
|
||||
/*
|
||||
sb.insert(2,c);
|
||||
sb.insert(2,j);
|
||||
sb.insert(2,b);
|
||||
sb.insert(2,"abc");
|
||||
*/
|
||||
String s = sb.toString();
|
||||
System.out.println(s);
|
||||
assert(s.equals("he123llo"));
|
||||
//assert(s.equals("heabctrue123/123llo"));
|
||||
//assert(!s.equals("heabctrue123/123llo"));
|
||||
}
|
||||
}
|
|
@ -0,0 +1,13 @@
|
|||
CORE
|
||||
test_int.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_int.java line 8: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_int.java line 9: SUCCESS$
|
||||
^\[assertion.3\] assertion at file test_int.java line 12: SUCCESS$
|
||||
^\[assertion.4\] assertion at file test_int.java line 15: SUCCESS$
|
||||
^\[assertion.5\] assertion at file test_int.java line 18: SUCCESS$
|
||||
^\[assertion.6\] assertion at file test_int.java line 21: SUCCESS$
|
||||
^\[assertion.7\] assertion at file test_int.java line 23: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,25 @@
|
|||
public class test_int {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
String s = Integer.toString(2345);
|
||||
char c = s.charAt(1);
|
||||
char d = s.charAt(2);
|
||||
char e = s.charAt(3);
|
||||
assert(c == '3');
|
||||
assert(d == '4');
|
||||
|
||||
int i = Integer.parseInt("1234");
|
||||
assert(i == 1234);
|
||||
|
||||
String t = Integer.toString(-2345);
|
||||
assert(t.charAt(0) == '-');
|
||||
|
||||
int j = Integer.parseInt("-4231");
|
||||
assert(j == -4231);
|
||||
|
||||
String u = Integer.toHexString(43981);
|
||||
assert(u.equals("abcd"));
|
||||
|
||||
assert(e == '2' || i < 1234 || t.charAt(0) != '-' || j != -4231 || !u.equals("abcd"));
|
||||
}
|
||||
}
|
|
@ -0,0 +1,10 @@
|
|||
CORE
|
||||
test_prefix.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_prefix.java line 14: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_prefix.java line 16: FAILURE$
|
||||
^\[assertion.3\] assertion at file test_prefix.java line 18: SUCCESS$
|
||||
^\[assertion.4\] assertion at file test_prefix.java line 20: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,23 @@
|
|||
public class test_prefix {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
String s = new String("Hello World!");
|
||||
//String t = new String("Hello");
|
||||
//String u = new String("Wello");
|
||||
String u = "Wello";
|
||||
boolean b = s.startsWith("Hello");
|
||||
//boolean c = s.startsWith("Wello");
|
||||
//boolean b = s.startsWith(t);
|
||||
boolean c = s.startsWith(u);
|
||||
boolean d = s.startsWith("lo",3);
|
||||
if(argv.length == 1){
|
||||
assert(b);
|
||||
} else if(argv.length == 2){
|
||||
assert(c);
|
||||
} else if(argv.length == 3){
|
||||
assert(d);
|
||||
} else if(argv.length == 4){
|
||||
assert(!d);
|
||||
}
|
||||
}
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
test_replace.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_replace.java line 6: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_replace.java line 8: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,10 @@
|
|||
public class test_replace {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
String s = new String("Hello World!");
|
||||
String t = s.replace('o','u');
|
||||
assert(t.equals("Hellu Wurld!"));
|
||||
System.out.println(t);
|
||||
assert(!t.equals("Hellu Wurld!"));
|
||||
}
|
||||
}
|
|
@ -0,0 +1,9 @@
|
|||
CORE
|
||||
test_set_length.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_set_length.java line 8: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_set_length.java line 9: SUCCESS$
|
||||
^\[assertion.3\] assertion at file test_set_length.java line 10: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,12 @@
|
|||
public class test_set_length {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
|
||||
StringBuilder s = new StringBuilder("abc");
|
||||
s.setLength(10);
|
||||
String t = s.toString();
|
||||
assert(t.startsWith("abc"));
|
||||
assert(t.length() == 10);
|
||||
assert(t.length() == 3);
|
||||
}
|
||||
}
|
|
@ -0,0 +1,9 @@
|
|||
CORE
|
||||
test_string_builder.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_string_builder.java line 11: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_string_builder.java line 12: SUCCESS$
|
||||
^\[assertion.3\] assertion at file test_string_builder.java line 13: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,16 @@
|
|||
public class test_string_builder {
|
||||
public static void main(String[] argv) {
|
||||
if(argv.length > 2) {
|
||||
StringBuilder tmp = new StringBuilder();
|
||||
tmp.append("prefix ");
|
||||
tmp.append(argv[1]);
|
||||
tmp.append(" middle ").append(argv[2]).append(" end");
|
||||
//StringBuilder tmp1 = tmp.append(argv[2]);
|
||||
//tmp1.append(" end");
|
||||
String r = tmp.toString();
|
||||
assert(r.startsWith("pref"));
|
||||
assert(r.endsWith("end"));
|
||||
assert(r.startsWith("pr3f"));
|
||||
}
|
||||
}
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
test_sb_length.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
\[assertion.1\] assertion at file test_sb_length.java line 6: SUCCESS$
|
||||
\[assertion.2\] assertion at file test_sb_length.java line 8: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,11 @@
|
|||
public class test_sb_length {
|
||||
public static void main(String[] argv) {
|
||||
StringBuilder tmp = new StringBuilder("prefix");
|
||||
//tmp.append("prefix");
|
||||
tmp.append("end");
|
||||
assert(tmp.length() == 9);
|
||||
if(argv.length > 1) {
|
||||
assert(tmp.length() == 12);
|
||||
}
|
||||
}
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
test_length.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_length.java line 10: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_length.java line 11: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,14 @@
|
|||
public class test_length {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
String s = new String("hello");
|
||||
if(argv.length > 1) {
|
||||
String t = argv[1];
|
||||
int i = t.length();
|
||||
String u = t.concat(s);
|
||||
char c = u.charAt(i);
|
||||
assert(c == 'h');
|
||||
assert(c == 'o');
|
||||
}
|
||||
}
|
||||
}
|
|
@ -0,0 +1,10 @@
|
|||
CORE
|
||||
test_substring.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_substring.java line 12: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_substring.java line 13: FAILURE$
|
||||
^\[assertion.3\] assertion at file test_substring.java line 20: SUCCESS$
|
||||
^\[assertion.4\] assertion at file test_substring.java line 21: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,27 @@
|
|||
public class test_substring {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
if(argv.length > 1) {
|
||||
String t = argv[1];
|
||||
|
||||
if(t.length() == 6) {
|
||||
String u = t.substring(2,4);
|
||||
char c = u.charAt(1);
|
||||
char d = t.charAt(3);
|
||||
char e = t.charAt(4);
|
||||
assert(c == d);
|
||||
assert(c == e);
|
||||
}
|
||||
else if(t.length() == 5){
|
||||
CharSequence u = t.subSequence(2,4);
|
||||
char c = u.charAt(1);
|
||||
char d = t.charAt(3);
|
||||
char e = t.charAt(4);
|
||||
assert(c == d);
|
||||
assert(c == e);
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
}
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
test_suffix.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_suffix.java line 12: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_suffix.java line 13: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,15 @@
|
|||
public class test_suffix {
|
||||
|
||||
public static void main(String[] argv) {
|
||||
String s = new String("Hello World!");
|
||||
//String t = new String("Hello");
|
||||
//String u = new String("Wello");
|
||||
String u = "Wello!";
|
||||
boolean b = s.endsWith("World!");
|
||||
//boolean c = s.startsWith("Wello");
|
||||
//boolean b = s.startsWith(t);
|
||||
boolean c = s.startsWith(u);
|
||||
assert(b);
|
||||
assert(c);
|
||||
}
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
test_trim.class
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[assertion.1\] assertion at file test_trim.java line 5: SUCCESS$
|
||||
^\[assertion.2\] assertion at file test_trim.java line 6: FAILURE$
|
||||
--
|
Binary file not shown.
|
@ -0,0 +1,8 @@
|
|||
public class test_trim {
|
||||
public static void main(String[] argv) {
|
||||
String t = " a b c ";
|
||||
String x = t.trim();
|
||||
assert(x.equals("a b c"));
|
||||
assert(x.equals("abc "));
|
||||
}
|
||||
}
|
|
@ -0,0 +1,18 @@
|
|||
#include <assert.h>
|
||||
#include "../cprover-string-hack.h"
|
||||
|
||||
|
||||
int main()
|
||||
{
|
||||
__CPROVER_string s;
|
||||
__CPROVER_char c1, c2;
|
||||
int i;
|
||||
int j;
|
||||
i = 2;
|
||||
s = __CPROVER_string_literal("pippo");
|
||||
c1 = __CPROVER_char_at(s, i);
|
||||
c2 = __CPROVER_char_literal("p");
|
||||
assert (c1 == c2);
|
||||
assert (c1 != c2);
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
test.c
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[main.assertion.1\] assertion c1 == c2: SUCCESS$
|
||||
^\[main.assertion.2\] assertion c1 != c2: FAILURE$
|
||||
--
|
|
@ -0,0 +1,13 @@
|
|||
#include <assert.h>
|
||||
#include "../cprover-string-hack.h"
|
||||
|
||||
int main()
|
||||
{
|
||||
__CPROVER_string s;
|
||||
int n;
|
||||
s = __CPROVER_string_literal("pippo");
|
||||
n = __CPROVER_string_length(s);
|
||||
assert(n == 5);
|
||||
assert(n != 5);
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
test.c
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[main.assertion.1\] assertion n == 5: SUCCESS$
|
||||
^\[main.assertion.2\] assertion n != 5: FAILURE$
|
||||
--
|
|
@ -0,0 +1,20 @@
|
|||
#include <assert.h>
|
||||
#include "../cprover-string-hack.h"
|
||||
|
||||
|
||||
int main()
|
||||
{
|
||||
__CPROVER_string s, s2, s3;
|
||||
int i;
|
||||
|
||||
s = __CPROVER_string_concat(s2, s3);
|
||||
__CPROVER_assume(__CPROVER_string_length(s2) == i);
|
||||
__CPROVER_assume(__CPROVER_string_equal(s3, __CPROVER_string_literal("pippo")));
|
||||
|
||||
// proving the assertions individually seems to be much faster
|
||||
assert(__CPROVER_string_length(s) == i + 5);
|
||||
//assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"), s));
|
||||
//assert(__CPROVER_char_at(s, i) == __CPROVER_char_literal("p"));
|
||||
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,7 @@
|
|||
CORE
|
||||
test.c
|
||||
--pass
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
|
@ -0,0 +1,22 @@
|
|||
#include <assert.h>
|
||||
#include "../cprover-string-hack.h"
|
||||
|
||||
|
||||
int main()
|
||||
{
|
||||
__CPROVER_string s, s2, s3;
|
||||
int i;
|
||||
|
||||
//__CPROVER_assume(i < 10);
|
||||
//__CPROVER_assume(__CPROVER_string_equal(s3, __CPROVER_string_literal("pippo")));
|
||||
s3 = __CPROVER_string_literal("pippo");
|
||||
s = __CPROVER_string_concat(s2, s3);
|
||||
__CPROVER_assume(__CPROVER_string_length(s2) == i);
|
||||
|
||||
// proving the assertions individually seems to be much faster
|
||||
//assert(__CPROVER_string_length(s) == i + 5);
|
||||
assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"),s));
|
||||
//assert(__CPROVER_char_at(s, i) == __CPROVER_char_literal("p"));
|
||||
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,7 @@
|
|||
CORE
|
||||
test.c
|
||||
--pass
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
|
@ -0,0 +1,22 @@
|
|||
#include <assert.h>
|
||||
#include "../cprover-string-hack.h"
|
||||
|
||||
|
||||
int main()
|
||||
{
|
||||
__CPROVER_string s, s2, s3;
|
||||
int i;
|
||||
|
||||
s = __CPROVER_string_concat(s2, s3);
|
||||
__CPROVER_assume(i < 10);
|
||||
__CPROVER_assume(__CPROVER_string_length(s2) == i);
|
||||
__CPROVER_assume(
|
||||
__CPROVER_string_equal(s3, __CPROVER_string_literal("pippo")));
|
||||
|
||||
// proving the assertions individually seems to be much faster
|
||||
//assert(__CPROVER_string_length(s) == i + 5);
|
||||
//assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"), s));
|
||||
assert(__CPROVER_char_at(s, i) == __CPROVER_char_literal("p"));
|
||||
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,7 @@
|
|||
CORE
|
||||
test.c
|
||||
--pass
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
|
@ -0,0 +1,18 @@
|
|||
#include <assert.h>
|
||||
#include "../cprover-string-hack.h"
|
||||
|
||||
|
||||
int main()
|
||||
{
|
||||
__CPROVER_string s, s2, s3;
|
||||
int i;
|
||||
|
||||
s = __CPROVER_string_concat(s2, s3);
|
||||
__CPROVER_assume(__CPROVER_string_length(s2) == i);
|
||||
__CPROVER_assume(
|
||||
__CPROVER_string_equal(s3, __CPROVER_string_literal("pippo")));
|
||||
|
||||
assert(__CPROVER_string_issuffix(__CPROVER_string_literal("p!o"), s));
|
||||
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,7 @@
|
|||
CORE
|
||||
test.c
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
|
@ -0,0 +1,37 @@
|
|||
(set-option :produce-models true)
|
||||
(set-logic ALL_SUPPORTED)
|
||||
|
||||
(declare-fun s () String)
|
||||
(declare-fun s2 () String)
|
||||
(declare-fun s3 () String)
|
||||
|
||||
(define-sort cprover.Pos () (_ BitVec 32))
|
||||
(define-fun cprover.ubv_to_int ((?x cprover.Pos)) Int (let ((bit0 (_ bv0 1)))
|
||||
(+ (ite (= ((_ extract 0 0) ?x) bit0) 0 1) (ite (= ((_ extract 1 1) ?x) bit0) 0 2) (ite (= ((_ extract 2 2) ?x) bit0) 0 4) (ite (= ((_ extract 3 3) ?x) bit0) 0 8) (ite (= ((_ extract 4 4) ?x) bit0) 0 16) (ite (= ((_ extract 5 5) ?x) bit0) 0 32) (ite (= ((_ extract 6 6) ?x) bit0) 0 64) (ite (= ((_ extract 7 7) ?x) bit0) 0 128) (ite (= ((_ extract 8 8) ?x) bit0) 0 256) (ite (= ((_ extract 9 9) ?x) bit0) 0 512) (ite (= ((_ extract 10 10) ?x) bit0) 0 1024) (ite (= ((_ extract 11 11) ?x) bit0) 0 2048) (ite (= ((_ extract 12 12) ?x) bit0) 0 4096) (ite (= ((_ extract 13 13) ?x) bit0) 0 8192) (ite (= ((_ extract 14 14) ?x) bit0) 0 16384) (ite (= ((_ extract 15 15) ?x) bit0) 0 32768) (ite (= ((_ extract 16 16) ?x) bit0) 0 65536) (ite (= ((_ extract 17 17) ?x) bit0) 0 131072) (ite (= ((_ extract 18 18) ?x) bit0) 0 262144) (ite (= ((_ extract 19 19) ?x) bit0) 0 524288) (ite (= ((_ extract 20 20) ?x) bit0) 0 1048576) (ite (= ((_ extract 21 21) ?x) bit0) 0 2097152) (ite (= ((_ extract 22 22) ?x) bit0) 0 4194304) (ite (= ((_ extract 23 23) ?x) bit0) 0 8388608) (ite (= ((_ extract 24 24) ?x) bit0) 0 16777216) (ite (= ((_ extract 25 25) ?x) bit0) 0 33554432) (ite (= ((_ extract 26 26) ?x) bit0) 0 67108864) (ite (= ((_ extract 27 27) ?x) bit0) 0 134217728) (ite (= ((_ extract 28 28) ?x) bit0) 0 268435456) (ite (= ((_ extract 29 29) ?x) bit0) 0 536870912) (ite (= ((_ extract 30 30) ?x) bit0) 0 1073741824) (ite (= ((_ extract 31 31) ?x) bit0) 0 2147483648) 0)))
|
||||
|
||||
(declare-fun bvi () cprover.Pos)
|
||||
(define-fun i () Int (cprover.ubv_to_int bvi))
|
||||
|
||||
(assert (= s (str.++ s2 s3)))
|
||||
|
||||
(assert (= (str.len s2) i))
|
||||
(assert (= s3 "pippo"))
|
||||
|
||||
(define-fun p1 () Bool (= (str.len s) (+ i 5)))
|
||||
(define-fun p2 () Bool (str.suffixof "po" s))
|
||||
(define-fun p3 () Bool (= (str.at s i) "p"))
|
||||
|
||||
(push 1)
|
||||
(assert (not p1))
|
||||
(check-sat)
|
||||
(pop 1)
|
||||
|
||||
(push 1)
|
||||
(assert (not p2))
|
||||
(check-sat)
|
||||
(pop 1)
|
||||
|
||||
(push 1)
|
||||
(assert (not p3))
|
||||
(check-sat)
|
||||
(pop 1)
|
|
@ -0,0 +1,25 @@
|
|||
(set-option :produce-models true)
|
||||
(set-logic ALL_SUPPORTED)
|
||||
|
||||
(declare-fun s () String)
|
||||
(declare-fun s2 () String)
|
||||
(declare-fun s3 () String)
|
||||
|
||||
(define-sort cprover.Pos () (_ BitVec 32))
|
||||
(define-fun cprover.ubv_to_int ((?x cprover.Pos)) Int (let ((bit0 (_ bv0 1)))
|
||||
(+ (ite (= ((_ extract 0 0) ?x) bit0) 0 1) (ite (= ((_ extract 1 1) ?x) bit0) 0 2) (ite (= ((_ extract 2 2) ?x) bit0) 0 4) (ite (= ((_ extract 3 3) ?x) bit0) 0 8) (ite (= ((_ extract 4 4) ?x) bit0) 0 16) (ite (= ((_ extract 5 5) ?x) bit0) 0 32) (ite (= ((_ extract 6 6) ?x) bit0) 0 64) (ite (= ((_ extract 7 7) ?x) bit0) 0 128) (ite (= ((_ extract 8 8) ?x) bit0) 0 256) (ite (= ((_ extract 9 9) ?x) bit0) 0 512) (ite (= ((_ extract 10 10) ?x) bit0) 0 1024) (ite (= ((_ extract 11 11) ?x) bit0) 0 2048) (ite (= ((_ extract 12 12) ?x) bit0) 0 4096) (ite (= ((_ extract 13 13) ?x) bit0) 0 8192) (ite (= ((_ extract 14 14) ?x) bit0) 0 16384) (ite (= ((_ extract 15 15) ?x) bit0) 0 32768) (ite (= ((_ extract 16 16) ?x) bit0) 0 65536) (ite (= ((_ extract 17 17) ?x) bit0) 0 131072) (ite (= ((_ extract 18 18) ?x) bit0) 0 262144) (ite (= ((_ extract 19 19) ?x) bit0) 0 524288) (ite (= ((_ extract 20 20) ?x) bit0) 0 1048576) (ite (= ((_ extract 21 21) ?x) bit0) 0 2097152) (ite (= ((_ extract 22 22) ?x) bit0) 0 4194304) (ite (= ((_ extract 23 23) ?x) bit0) 0 8388608) (ite (= ((_ extract 24 24) ?x) bit0) 0 16777216) (ite (= ((_ extract 25 25) ?x) bit0) 0 33554432) (ite (= ((_ extract 26 26) ?x) bit0) 0 67108864) (ite (= ((_ extract 27 27) ?x) bit0) 0 134217728) (ite (= ((_ extract 28 28) ?x) bit0) 0 268435456) (ite (= ((_ extract 29 29) ?x) bit0) 0 536870912) (ite (= ((_ extract 30 30) ?x) bit0) 0 1073741824) (ite (= ((_ extract 31 31) ?x) bit0) 0 2147483648) 0)))
|
||||
|
||||
(declare-fun bvi () cprover.Pos)
|
||||
(define-fun i () Int (cprover.ubv_to_int bvi))
|
||||
|
||||
(assert (= s (str.++ s2 s3)))
|
||||
|
||||
(assert (= (str.len s2) i))
|
||||
(assert (= s3 "pippo"))
|
||||
|
||||
(define-fun p1 () Bool (= (str.len s) (+ i 5)))
|
||||
(define-fun p2 () Bool (str.suffixof "po" s))
|
||||
(define-fun p3 () Bool (= (str.at s i) "p"))
|
||||
|
||||
(assert (or (not p1) (not p2) (not p3)))
|
||||
(check-sat)
|
|
@ -0,0 +1,20 @@
|
|||
(set-option :produce-models true)
|
||||
(set-logic ALL_SUPPORTED)
|
||||
|
||||
(declare-fun s () String)
|
||||
(declare-fun s2 () String)
|
||||
(declare-fun s3 () String)
|
||||
|
||||
(declare-fun i () Int)
|
||||
|
||||
(assert (= s (str.++ s2 s3)))
|
||||
|
||||
(assert (= (str.len s2) i))
|
||||
(assert (= s3 "pippo"))
|
||||
|
||||
(define-fun p1 () Bool (= (str.len s) (+ i 5)))
|
||||
(define-fun p2 () Bool (str.suffixof "po" s))
|
||||
(define-fun p3 () Bool (= (str.at s i) "p"))
|
||||
|
||||
(assert (or (not p1) (not p2) (not p3)))
|
||||
(check-sat)
|
|
@ -0,0 +1,21 @@
|
|||
#include <assert.h>
|
||||
#include "../cprover-string-hack.h"
|
||||
|
||||
|
||||
int main()
|
||||
{
|
||||
__CPROVER_string s, s2, s3;
|
||||
int i;
|
||||
|
||||
s = __CPROVER_string_concat(s2, s3);
|
||||
__CPROVER_assume(__CPROVER_string_length(s2) == i);
|
||||
__CPROVER_assume(
|
||||
__CPROVER_string_equal(s3, __CPROVER_string_literal("pippo")));
|
||||
|
||||
assert(__CPROVER_string_length(s) == i + 5);
|
||||
assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"),s));
|
||||
assert(__CPROVER_char_at(s, i) == __CPROVER_char_literal("p"));
|
||||
assert(__CPROVER_string_issuffix(__CPROVER_string_literal("p!o"), s));
|
||||
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,10 @@
|
|||
CORE
|
||||
test.c
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_length_func(s) == i + 5: SUCCESS$
|
||||
^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"po\"), s): SUCCESS$
|
||||
^\[main.assertion.3\] assertion __CPROVER_uninterpreted_string_char_at_func(s, i) == __CPROVER_uninterpreted_char_literal_func(\"p\"): SUCCESS$
|
||||
^\[main.assertion.4\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"p!o\"), s): FAILURE$
|
||||
--
|
|
@ -0,0 +1,17 @@
|
|||
#include <assert.h>
|
||||
#include "../cprover-string-hack.h"
|
||||
|
||||
|
||||
int main()
|
||||
{
|
||||
__CPROVER_string s;
|
||||
int i;
|
||||
int j;
|
||||
i = 2;
|
||||
s = __CPROVER_string_literal("pippo");
|
||||
if (__CPROVER_char_at(s, i) == __CPROVER_char_literal("p")) {
|
||||
j = 1;
|
||||
}
|
||||
assert(j == 1);
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,7 @@
|
|||
CORE
|
||||
test.c
|
||||
--pass
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
|
@ -0,0 +1,14 @@
|
|||
#include <assert.h>
|
||||
#include "../cprover-string-hack.h"
|
||||
|
||||
|
||||
void main()
|
||||
{
|
||||
__CPROVER_string x, y, z, w;
|
||||
|
||||
if (__CPROVER_string_equal(z, __CPROVER_string_concat(x, y)) &&
|
||||
__CPROVER_string_equal(z, __CPROVER_string_concat(w, __CPROVER_string_literal("c"))) &&
|
||||
__CPROVER_string_equal(__CPROVER_string_concat(__CPROVER_string_literal("c"), y), __CPROVER_string_concat(__CPROVER_string_literal("c"), __CPROVER_string_concat(__CPROVER_string_literal("b"), __CPROVER_string_literal("c"))))) {
|
||||
assert(0);
|
||||
}
|
||||
}
|
|
@ -0,0 +1,7 @@
|
|||
CORE
|
||||
test.c
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION FAILED$
|
||||
--
|
|
@ -0,0 +1,14 @@
|
|||
#include <assert.h>
|
||||
#include "../cprover-string-hack.h"
|
||||
|
||||
|
||||
int main()
|
||||
{
|
||||
__CPROVER_string s = __CPROVER_string_literal("abc");;
|
||||
char c = 'p';
|
||||
__CPROVER_string t = __CPROVER_char_set(s,1,c);;
|
||||
|
||||
assert(__CPROVER_string_equal(t, __CPROVER_string_literal("apc")));
|
||||
assert(__CPROVER_string_equal(t, __CPROVER_string_literal("abc")));
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
test.c
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func("apc")): SUCCESS$
|
||||
^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func("abc")): FAILURE$
|
||||
--
|
|
@ -0,0 +1,16 @@
|
|||
#include <assert.h>
|
||||
#include "../cprover-string-hack.h"
|
||||
|
||||
|
||||
int main()
|
||||
{
|
||||
__CPROVER_string s,t,u;
|
||||
unsigned i = __CPROVER_string_length(s);
|
||||
t = __CPROVER_string_literal("ppo");
|
||||
u = __CPROVER_string_concat(s, t);
|
||||
__CPROVER_char c = __CPROVER_char_at(u,i);
|
||||
|
||||
assert(c == __CPROVER_char_literal("p"));
|
||||
assert(__CPROVER_char_at(u,2) == __CPROVER_char_literal("p"));
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
test.c
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[main.assertion.1\] assertion c == __CPROVER_uninterpreted_char_literal_func(\"p\"): SUCCESS$
|
||||
^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_char_at_func(u, 2) == __CPROVER_uninterpreted_char_literal_func(\"p\"): FAILURE$
|
||||
--
|
|
@ -0,0 +1,22 @@
|
|||
#include <assert.h>
|
||||
#include "../cprover-string-hack.h"
|
||||
|
||||
|
||||
int main()
|
||||
{
|
||||
__CPROVER_string s1 = __CPROVER_string_literal("a1");
|
||||
__CPROVER_string s2 = __CPROVER_string_literal("2b");
|
||||
__CPROVER_string t = __CPROVER_string_concat(s1, s2);
|
||||
|
||||
int i = nondet_int();
|
||||
|
||||
|
||||
if(i==1)
|
||||
assert(!__CPROVER_string_contains(t,__CPROVER_string_literal("3")));
|
||||
else if(i==2)
|
||||
assert(__CPROVER_string_contains(t,__CPROVER_string_literal("12")));
|
||||
else if(i==3)
|
||||
assert(!__CPROVER_string_contains(t,__CPROVER_string_literal("b")));
|
||||
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,9 @@
|
|||
KNOWNBUG
|
||||
test.c
|
||||
--pass
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
^\[main.assertion.1\] assertion !__CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"3\")): SUCCESS$
|
||||
^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"12\")): SUCCESS$
|
||||
^\[main.assertion.3\] assertion !__CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"b\")): FAILURE$
|
||||
--
|
|
@ -0,0 +1,43 @@
|
|||
#include <assert.h>
|
||||
#include "../cprover-string-hack.h"
|
||||
#define false 0
|
||||
#define true 1
|
||||
|
||||
int main(){
|
||||
//IsEasyChairQuery
|
||||
__CPROVER_string str;
|
||||
// (1) check that str contains "/" followed by anything not
|
||||
// containing "/" and containing "EasyChair"
|
||||
int lastSlash = __CPROVER_string_last_index_of(str,__CPROVER_char_literal("/"));
|
||||
if(lastSlash < 0) {
|
||||
__CPROVER_assert(false,"PC1");
|
||||
return false;
|
||||
}
|
||||
|
||||
__CPROVER_string rest = __CPROVER_string_substring(str,lastSlash + 1, __CPROVER_string_length(str)-1);
|
||||
|
||||
if(! __CPROVER_string_contains(rest,__CPROVER_string_literal("EasyChair"))) {
|
||||
__CPROVER_assert(false,"PC2");
|
||||
return false;
|
||||
}
|
||||
|
||||
// (2) Check that str starts with "http://"
|
||||
if(! __CPROVER_string_isprefix(__CPROVER_string_literal("http://"),str)) {
|
||||
__CPROVER_assert(false,"PC3");
|
||||
return false;
|
||||
}
|
||||
//(3) Take the string between "http://" and the last "/".
|
||||
// if it starts with "www." strip the "www." off
|
||||
__CPROVER_string t = __CPROVER_string_substring(str,__CPROVER_string_length(__CPROVER_string_literal("http://")), lastSlash - __CPROVER_string_length(__CPROVER_string_literal("http://")));
|
||||
if(__CPROVER_string_isprefix(__CPROVER_string_literal("www."),t))
|
||||
t = __CPROVER_string_substring(t,__CPROVER_string_length(__CPROVER_string_literal("www.")), __CPROVER_string_length(t)-1);
|
||||
// (4) Check that after stripping we have either "live.com"
|
||||
// or "google.com"
|
||||
if (!__CPROVER_string_equal(t,__CPROVER_string_literal("live.com")) && !__CPROVER_string_equal(t,__CPROVER_string_literal( "google.com"))) {
|
||||
__CPROVER_assert(false,"PC4");
|
||||
return false;
|
||||
}
|
||||
// s survived all checks
|
||||
return true;
|
||||
}
|
||||
|
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue