我想知道GCC为每个编译单元集合生成了多少目标代码,但是我遇到了一个奇怪的问题,即来自binutils的"size"命令没有给出正确的结果.
我们来看一个只包含这个函数的C文件:
int foo (int a, int b)
{
return a+b;
}
我们可以编译它并使用"size"和"objdump"检查目标代码大小:
$ gcc -O foo.c -c
$ size foo.o
text data bss dec hex filename
52 0 0 52 34 foo.o
$ objdump -d foo.o
foo.o: file format elf64-x86-64
Disassembly of section .text:
0000000000000000 <foo>:
0: 8d 04 37 lea (%rdi,%rsi,1),%eax
3: c3 retq
从objdump输出中可以清楚地看出,目标代码大小是4个字节.但是,大小报告52个字节,这是不正确的.
从使用"-D"选项到objdump,它看起来像异常处理代码,也许其他一些东西正在通过"大小"来衡量,并添加到我真正关心的代码的大小.有没有人知道一个相对简单的方法来获得大小忽略这些额外的东西？
z3 的 C API 具有 Z3_mk_bvadd_no_overflow 等函数，但这些函数似乎无法从 Python API 中获得。在我开始破解这个问题之前，我只想验证一下情况是否如此，并请求将这些添加到正式版本中。
我正在尝试将类似的内容添加到 z3.py 中，但到目前为止尚未设法获得正确的详细信息。关于我哪里出错的建议将不胜感激。我正在 contrib 分支工作。
def Bvadd_no_overflow(a, b, si, ctx=None):
"""Create a Z3 bvadd_no_overflow expression.
"""
ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
# argh can't hard-code the 32
s = BitVecSort(32,ctx)
a = s.cast(a)
b = s.cast(b)
# this function requires a bool as the last argument but is it a python bool, a
# z3 bool, or what?
return BitVecRef(Z3_mk_bvadd_no_overflow(ctx.ref(), a.as_ast(), b.as_ast(), 1), ctx)