blob: fcdcded39c93d95f51a86e26bc6498f8f5b6310c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
(set-info :smt-lib-version 2.6)
(set-option :strings-exp true)
(declare-fun value () String)
(declare-fun name () String)
(assert (not (not (not (= (ite (str.contains value "?") 1 0) 0)))))
(assert (not (not (= (ite (str.contains value "#") 1 0) 0))))
(assert (not (not (= (ite (= (str.substr value 0 (- 2 0)) "//") 1 0) 0))))
(assert (not (not (= (ite (> (str.indexof value ":" 0) 0) 1 0) 0))))
(assert (not (= (ite (not (= (str.len value) 0)) 1 0) 0)))
(assert (not (not (= (ite (str.contains value "'") 1 0) 0))))
(assert (not (not (= (ite (str.contains value "\\""") 1 0) 0))))
(assert (not (not (= (ite (str.contains value ">") 1 0) 0))))
(assert (not (not (= (ite (str.contains value "<") 1 0) 0))))
(assert (not (not (= (ite (str.contains value "&") 1 0) 0))))
(assert (not (not (= (ite (str.contains name "'") 1 0) 0))))
(assert (not (not (= (ite (str.contains name "\\""") 1 0) 0))))
(assert (not (not (= (ite (str.contains name ">") 1 0) 0))))
(assert (not (not (= (ite (str.contains name "<") 1 0) 0))))
(assert (not (not (= (ite (str.contains name "&") 1 0) 0))))
(assert (not (= (ite (not (= value "")) 1 0) 0)))
(assert (not (= (ite (str.contains value "javascript:alert(1);") 1 0) 0)))
(assert (not (not (= (ite (str.contains name "javascript:alert(1);") 1 0) 0))))
(check-sat)
|
