blob: 0e0ef063ccde5b15b0a6dde2197cd631f48c4ef1 (
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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
#!/usr/bin/env python3
#####################
## interactive_shell.py
## Top contributors (to current version):
## Andrew V. Jones
## This file is part of the CVC4 project.
## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
## in the top-level source directory and their institutional affiliations.
## All rights reserved. See the file COPYING in the top-level source
## directory for licensing information.
##
#####################
#! \file interactive_shell.py
## \verbatim
## Top contributors (to current version):
## Andrew V. Jones
## This file is part of the CVC4 project.
## Copyright (c) 2020 by the authors listed in the file AUTHORS
## in the top-level source directory) and their institutional affiliations.
## All rights reserved. See the file COPYING in the top-level source
## directory for licensing information.\endverbatim
##
## \brief A simple test file to interact with CVC4 with line editing
#####################
import sys
import pexpect
def check_iteractive_shell():
"""
Interacts with CVC4's interactive shell and checks that things such a tab
completion and "pressing up" works.
"""
# Open CVC4
child = pexpect.spawnu("bin/cvc4", timeout=1)
# We expect to see the CVC4 prompt
child.expect("CVC4>")
# If we send a line with just 'BOOLE' ...
child.sendline("BOOLE")
# ... then we get an error
child.expect("Parse Error: <shell>:...: Unexpected token: 'BOOLE'")
# Start sending 'BOOL' (without an E)
child.send("BOOL")
# Send tab twice
child.sendcontrol("i")
child.sendcontrol("i")
# We expect to see the completion
child.expect("BOOL.*BOOLEAN.*BOOLEXTRACT")
# NOTE: the double tab has completed our 'BOOL' to 'BOOLE'!
# Now send enter (which submits 'BOOLE')
child.sendcontrol("m")
# So we expect to see an error for 'BOOLE'
child.expect("Parse Error: <shell>:...: Unexpected token: 'BOOLE'")
# Send enter
child.sendcontrol("m")
# We expect to see the CVC4 prompt
child.expect("CVC4>")
# Now send an up key
child.send("\033[A")
# Send enter
child.sendcontrol("m")
# We expect to see an error on 'BOOLE' again
child.expect("Parse Error: <shell>:...: Unexpected token: 'BOOLE'")
return 0
def main():
"""
Runs our interactive shell test
Caveats:
* If we don't have the "pexpect" model, the test doesn't get run, but
passes
* We expect pexpect to raise and exit with a non-zero exit code if any
of the steps fail
"""
# If any of the "steps" fail, the pexpect will raise a Python will exit
# with a non-zero error code
sys.exit(check_iteractive_shell())
if __name__ == "__main__":
main()
# EOF
|
