Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Failing compilation of random.c during benchmark testing on macOS #50

Open
gabryon99 opened this issue Jan 5, 2023 · 0 comments
Open
Labels
goblint Goblint-specific problem

Comments

@gabryon99
Copy link

When running the benchmark suit with the script ./update_bench.rb I get a failing compilation error on final results for char/random.c.


Error's output:

In file included from /Users/gabryon/University/TUM/static_analysis/Code/analyzer/linux-headers/include/linux/compiler.h:54,
                 from /Users/gabryon/University/TUM/static_analysis/Code/analyzer/linux-headers/include/uapi/linux/stddef.h:1,
                 from /Users/gabryon/University/TUM/static_analysis/Code/analyzer/linux-headers/include/linux/stddef.h:4,
                 from /Users/gabryon/University/TUM/static_analysis/Code/analyzer/linux-headers/include/uapi/linux/posix_types.h:4,
                 from /Users/gabryon/University/TUM/static_analysis/Code/analyzer/linux-headers/include/uapi/linux/types.h:13,
                 from /Users/gabryon/University/TUM/static_analysis/Code/analyzer/linux-headers/include/linux/types.h:5,
                 from /Users/gabryon/University/TUM/static_analysis/Code/analyzer/linux-headers/include/uapi/linux/capability.h:16,
                 from /Users/gabryon/University/TUM/static_analysis/Code/analyzer/linux-headers/include/linux/capability.h:15,
                 from /Users/gabryon/University/TUM/static_analysis/Code/analyzer/linux-headers/include/linux/sched.h:15,
                 from /Users/gabryon/University/TUM/static_analysis/Code/analyzer/linux-headers/include/linux/utsname.h:5,
                 from random.c:238:
/Users/gabryon/University/TUM/static_analysis/Code/analyzer/linux-headers/include/linux/compiler-gcc.h:68: warning: "__weak" redefined
   68 | #define __weak                          __attribute__((weak))
      | 
<built-in>: note: this is the location of the previous definition
random.c:1523: Warning: builtin_choose_expr expects a constant first argument
random.c:1523: Warning: builtin_choose_expr expects a constant first argument
random.c:1523: Warning: builtin_choose_expr expects a constant first argument
random.c:1523: Warning: builtin_choose_expr expects a constant first argument
random.c:1523: Warning: builtin_choose_expr expects a constant first argument
random.c:1523: Warning: builtin_choose_expr expects a constant first argument
random.c:1523: Warning: builtin_choose_expr expects a constant first argument
random.c:1523: Warning: builtin_choose_expr expects a constant first argument
random.c:1523: Warning: builtin_choose_expr expects a constant first argument
random.c:1523: Bug: formal buf is not in locals (found instead tmp___15)
  Context : 2cil: SyS_getrandom
error in collectFunction SyS_getrandom: GoblintCil__Errormsg.ErrorError: There were errors during merging

Fatal error: exception GoblintCil__Errormsg.Error

=== APPENDED BY BENCHMARKING SCRIPT ===
Analysis began: 2023-01-05 11:44:34 +0100
Analysis ended: 2023-01-05 11:44:36 +0100
Duration: 1.53 s
Goblint params: /Users/gabryon/University/TUM/static_analysis/Code/analyzer/goblint --set dbg.timeout 900  random.c --enable kernel --set otherfun "['rand_initialize', 'add_interrupt_randomness', 'sys_getrandom', 'SyS_getrandom', 'SYSC_getrandom', 'random_int_secret_init', 'randomize_range', 'rand_initialize_disk', 'add_device_randomness', 'add_input_randomness', 'add_disk_randomness', 'get_random_bytes', 'get_random_bytes_arch', 'generate_random_uuid', 'get_random_int', 'add_hwgenerator_randomness']"  --enable allglobs --enable dbg.timing.enabled 1>/Users/gabryon/University/TUM/static_analysis/Code/bench/bench_result/random.default.txt 2>&1
Goblint version: heads/IntervalSets-0-gdbb8079e9
Cil version:     2.0.0-21-g3d079de
Profile:         dev
EXITCODE                   2

Additional Information:

  • macOS 13.0.1 22A400 x86_64
  • gcc-12 (Homebrew GCC 12.2.0) 12.2.0
@michael-schwarz michael-schwarz added the goblint Goblint-specific problem label Jan 5, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
goblint Goblint-specific problem
Projects
None yet
Development

No branches or pull requests

2 participants