-
Notifications
You must be signed in to change notification settings - Fork 7
Open
Labels
goblintGoblint-specific problemGoblint-specific problemparsing-succeedsprojectProject to analyzeProject to analyze
Description
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-supportThen 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
bear -- make rsyncThen 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.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. - (Changed all
-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 sigaction which makes Goblint analysis multi-threaded, but this didn't help.
Metadata
Metadata
Assignees
Labels
goblintGoblint-specific problemGoblint-specific problemparsing-succeedsprojectProject to analyzeProject to analyze