search

goblint / bench

The benchmark suite
4 stars 5 forks source link

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

Open gabryon99 opened 1 year ago

gabryon99 commented 1 year ago

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: