blob: 86cc592fb2a5f34a3bea043bc195a4ba66505f46 (
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
|
(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)
|