gernst / legion-symcc

Fresh implementation of the Legion algorithm on top of SyMCC
Other
0 stars 1 forks source link

[TestComp-2022] `OUT OF MEMORY` with no output from `Legion-SymCC` #24

Open DonggeLiu opened 2 years ago

DonggeLiu commented 2 years ago

Issue

Legion-SymCC terminated without any output. It is worth noting that TestCov reported over 70% coverage on the corresponding programs. Maybe this implies this kind of OUT OF MEMORY is less important/urgent?

Full output from Legion-SymCC

./legion.sh -L ubuntu2004/lib -m 10000 -32 ../../sv-benchmarks/c/array-examples/standard_copy2_ground-1.i

--------------------------------------------------------------------------------

../../sv-benchmarks/c/array-examples/standard_copy2_ground-1.i:5:36: warning: unknown attribute '__leaf__' ignored [-Wunknown-attributes]
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
                                   ^
../../sv-benchmarks/c/array-examples/standard_copy2_ground-1.i:8:36: warning: unknown attribute '__leaf__' ignored [-Wunknown-attributes]
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
                                   ^
../../sv-benchmarks/c/array-examples/standard_copy2_ground-1.i:10:36: warning: unknown attribute '__leaf__' ignored [-Wunknown-attributes]
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
                                   ^
Symbolizer module init
Symbolizing function reach_error
Symbolizing function __VERIFIER_assert
Symbolizing function main
3 warnings generated.
Symbolizer module init
Symbolizing function __assert_fail
Symbolizing function __VERIFIER_nondet_bool
Symbolizing function __VERIFIER_nondet_char
Symbolizing function __VERIFIER_nondet_uchar
Symbolizing function __VERIFIER_nondet_short
Symbolizing function __VERIFIER_nondet_ushort
Symbolizing function __VERIFIER_nondet_unsigned_long
Symbolizing function __VERIFIER_nondet_long
Symbolizing function __VERIFIER_nondet_uint
Symbolizing function __VERIFIER_nondet_int
Symbolizing function __VERIFIER_nondet_unsigned
Symbolizing function __VERIFIER_nondet_ulong
Symbolizing function __VERIFIER_nondet_float
Symbolizing function __VERIFIER_nondet_double
Symbolizing function __VERIFIER_initialize

Command

./legion.sh -L ubuntu2004/lib -m 10000 -32 ../../sv-benchmarks/c/array-examples/standard_copy2_ground-1.i

Corresponding programs

array-examples/standard_copy1_ground-2.yml array-examples/standard_copy2_ground-1.yml array-examples/standard_copy3_ground-2.yml