diff --git a/tests/misc/array_sizeof.i b/tests/misc/array_sizeof.i index fa364f4725aac76c1268793f11fbb2b7d737c367..c857ad90a1b0f3dddaff3790a7ea5fccb2b7f24d 100644 --- a/tests/misc/array_sizeof.i +++ b/tests/misc/array_sizeof.i @@ -4,7 +4,14 @@ STDOPT: */ int x; -void main() { +void main(int c) { +if (c) { unsigned char buf[sizeof(unsigned char[1]) + sizeof(x)]; buf[sizeof(buf)]; } +else { + x = 4; + unsigned char buf[sizeof(unsigned char[1]) + x]; + buf[x]; +} +} diff --git a/tests/misc/oracle/array_sizeof.res.oracle b/tests/misc/oracle/array_sizeof.res.oracle index e580c4e07525d3a39e1a6ffc69cb23038a53307c..04709d7aeef10d123f254d881895f0173ef3a986 100644 --- a/tests/misc/oracle/array_sizeof.res.oracle +++ b/tests/misc/oracle/array_sizeof.res.oracle @@ -4,26 +4,37 @@ [eva] Initial state computed [eva:initial-state] Values of globals at initialization x ∈ {0} -[eva:alarm] array_sizeof.i:9: Warning: +[eva:alarm] array_sizeof.i:10: Warning: accessing out of bounds index. assert sizeof(unsigned char [sizeof(unsigned char [1]) + sizeof(x)]) < (unsigned int)(sizeof(unsigned char [1]) + sizeof(int)); +[eva] array_sizeof.i:14: assertion 'alloca_bounds' got status valid. +[eva] array_sizeof.i:14: Call to builtin __fc_vla_alloc +[eva] array_sizeof.i:14: allocating variable __malloc_main_l14 +[eva:alarm] array_sizeof.i:15: Warning: + accessing uninitialized left-value. assert \initialized(buf_0 + x); [eva] Recording results for main [eva] done for function main -[eva] array_sizeof.i:9: assertion 'Eva,index_bound' got final status invalid. +[eva] array_sizeof.i:10: assertion 'Eva,index_bound' got final status invalid. +[eva] array_sizeof.i:15: + assertion 'Eva,initialization' got final status invalid. [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function main: NON TERMINATING FUNCTION [from] Computing for function main +[from] Computing for function __fc_vla_alloc <-main +[from] Done for function __fc_vla_alloc [from] Non-terminating function main (no dependencies) [from] Done for function main [from] ====== DEPENDENCIES COMPUTED ====== These dependencies hold at termination for the executions that terminate: +[from] Function __fc_vla_alloc: + \result FROM \nothing [from] Function main: NON TERMINATING - NO EFFECTS [from] ====== END OF DEPENDENCIES ====== [inout] Out (internal) for function main: - tmp + x; tmp; buf_0; __lengthof_buf_0; tmp_3 [inout] Inputs for function main: - \nothing + x; __malloc_main_l14[4]