blob: 3098a59baab6c2c70b28351c672468ae3ac913be (
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
27
|
(set-info :smt-lib-version 2.6)
(set-logic QF_S)
(set-option :strings-exp true)
(set-info :status sat)
(declare-fun s () String)
;(assert (= s "</script><script>alert(1);</script><script>"))
(declare-fun joined () String)
(assert (= joined (str.++ "<script>console.log('" s "');</script>")))
(assert (str.contains joined "<script>alert(1);</script>"))
; (<script>[^<]*</script>)+
(assert (str.in_re joined
(re.+ (re.++
(str.to_re "<script>")
(re.*
(re.union
(re.range " " ";")
(re.range "=" "~")
)
)
(str.to_re "</script>")
))
))
(check-sat)
|
