blob: 3bf47ed61fd17d48f4725a9b47172708b40f0b81 (
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
|
; COMMAND-LINE: --lang=smt2.0
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
(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)
|
