我想编写Python代码以将文件从客户端发送到服务器.服务器需要保存从客户端发送的文件.但我的代码有一些我无法解决的错误.以下是我的服务器代码:
# server.py
from SimpleXMLRPCServer import SimpleXMLRPCServer
import os
server = SimpleXMLRPCServer(('localhost', 9000))
def save_data(data):
handle = open("x123.dat", "wb")
handle.write(data)
handle.close()
server.register_function(save_data, 'save_data')
server.serve_forever()
和客户端代码:
# client.py
import sys, xmlrpclib
proxy = xmlrpclib.Server('http://localhost:9000')
handle = open(sys.argv[1], "rb")
proxy.save_data(handle.read())
handle.close()
但后来我运行我的代码,客户端返回以下错误(这是在Windows上):
Traceback (most recent call last):
File "client.py", line 6, in <module> proxy.save_data(handle.read())
File "c:\python27\lib\xmlrpclib.py", line 1224, in __call__
return self.__send(self.__name, args)
File "c:\python27\lib\xmlrpclib.py", line 1575, in __request
verbose=self.__verbose
File "c:\python27\lib\xmlrpclib.py", line 1264, in request
return self.single_request(host, handler, request_body, verbose)
File …我有两个不同大小的'a'和'b'变量,见下文.我有几个问题:
(1)如何将'a'的值复制为'b'？(即延长操作)
(2)如何将'b'的值复制为'a'？(即截断操作)
谢谢.
a = BitVec('a', 1)
b = BitVec('b', 32)
给定Z3py中的表达式,我可以将其转换为SMT-LIB2语言吗？(所以我可以将这个SMT-LIB2表达式提供给支持SMT-LIB2的其他SMT求解器)
如果可以,请举一个例子.
非常感谢.
假设这a是一个8位值的整数254.如果a是有符号整数,则实际考虑它-2.相反,如果a是未签名的,它仍然存在254.
我试图用Z3的BitVector理论模拟这个有符号/无符号整数问题,但似乎BitVector不允许这样做.这是真的？那么关于如何在Z3py中对此进行建模的任何想法？
非常感谢.
我编写以下Z3 python代码
x, y = Ints('x y')
F = (x == y & 16) # x has the value of (y & 16)
print F
但我得到了以下错误:
TypeError: unsupported operand type(s) for &: 'instance' and 'int'
如何在Z3方程中进行按位运算(在这种情况下)？
谢谢.
我使用的是Z3 3.0版.我想为bitvector变量赋值,如下所示.但Z3报告错误"无效的功能应用程序,排序第3行位置2的参数不匹配".
我的常数#x0a似乎有问题？我怎样才能解决这个问题？
谢谢
(set-logic QF_BV)
(declare-fun a () (_ BitVec 32))
(assert (= a #x0a))
(check-sat)
我在IR中有一些代码,这段代码已经是SSA形式.现在我试图将此代码转换为SMT公式,然后将其提供给Z3进行一些验证.我有一些问题:
有没有技术论文详细解释如何将SSA IR转换为SMT公式？我四处搜索,无济于事.
对于那些计算指令,转换为Z3公式没有太多问题.但是,我仍在努力处理无条件和条件分支指令.有关如何将这些指令转换为Z3公式的任何建议？
非常感谢!!!
我想在Z3 python中对If-the-else进行编码,但是找不到任何关于如何做的文档或示例.
我有一个示例代码,如下所示.
F = True
tmp = BitVec('tmp', 1)
tmp1 = BitVec('tmp1', 8)
现在我该如何将这个条件编码为F:
if tmp == 1, then tmp1 == 100. otherwise, tmp1 == 0
非常感谢.
我在 Z3 python 中有这个代码：
x = Bool('x')
y = Bool('y')
z = Bool('z')
z == (x xor y)
s = Solver()
s.add(z == True)
print s.check()
但是此代码在运行时报告以下错误：
c.py(4): error: invalid syntax
如果我替换xor为and，则没有问题。所以这意味着不支持异或？