https://github.com/RsyncProject/rsync/
Initial attempt
Goblint version: heads/master-0-gd505a38c7
Checked out git tag v3.4.1 and executed
./configure --disable-md2man --disable-xxhash --disable-zstd --disable-lz4 --disable-iconv --disable-iconv-open --disable-openssl --disable-acl-support --disable-xattr-support
Then in config.h manually commented out #define USE_MD5_ASM 1 and #define USE_ROLL_SIMD 1. There are only --enable options for these and they're enabled by default, so there doesn't seem to be a way to disable them (they use C++ and ASM).
Then executed
Then in compile_commands.json manually did the following modifications:
- Removed
rounding.c. It's a helper program executed in the middle of the build to generate some header. Not sure why this isn't part of ./configure.
- Removed
simd-checksum-x86_64.cpp and md5-asm-x86_64.S. Even when defined to not be used, they're still compiled. But we don't want to try to merge them because parsing fails.
- (Changed all
-O2 arguments to -O0. Because -O2 disables fortified headers. Not actually necessary perhaps.)
Then executed
goblint compile_commands.json
but this doesn't yield to any result quickly.
I also tried
goblint compile_commands.json --set ana.base.strings.domain unit --enable exp.single-threaded
because a lot of the top functions in the solver stats are string/printing ones and rsync uses sigaction which makes Goblint analysis multi-threaded, but this didn't help.
https://github.com/RsyncProject/rsync/
Initial attempt
Goblint version: heads/master-0-gd505a38c7
Checked out git tag
v3.4.1and executed./configure --disable-md2man --disable-xxhash --disable-zstd --disable-lz4 --disable-iconv --disable-iconv-open --disable-openssl --disable-acl-support --disable-xattr-supportThen in
config.hmanually commented out#define USE_MD5_ASM 1and#define USE_ROLL_SIMD 1. There are only--enableoptions for these and they're enabled by default, so there doesn't seem to be a way to disable them (they use C++ and ASM).Then executed
bear -- make rsyncThen in
compile_commands.jsonmanually did the following modifications:rounding.c. It's a helper program executed in the middle of the build to generate some header. Not sure why this isn't part of./configure.simd-checksum-x86_64.cppandmd5-asm-x86_64.S. Even when defined to not be used, they're still compiled. But we don't want to try to merge them because parsing fails.-O2arguments to-O0. Because-O2disables fortified headers. Not actually necessary perhaps.)Then executed
goblint compile_commands.jsonbut this doesn't yield to any result quickly.
I also tried
goblint compile_commands.json --set ana.base.strings.domain unit --enable exp.single-threadedbecause a lot of the top functions in the solver stats are string/printing ones and rsync uses
sigactionwhich makes Goblint analysis multi-threaded, but this didn't help.