Bug #6574
open
Initialize callback parameters by default
Added by Ilja Zakharov over 8 years ago.
Updated over 8 years ago.
Category:
Environment models
Description
EMG allocates memory for default parameters for callbacks in case of structure pointers. Memory for the other pointers from parameters should be also allocated and initialized.
- Category set to Environment models
- Subject changed from Initialize defualt values to Initialize default values
- Description updated (diff)
I dislike "default values". Maybe "callback parameters" would be better.
- Subject changed from Initialize default values to Initialize callback parameters by default
Currently it is implemented in EMG but we need more:
- Configuration property or several ones to configure what and how to initialize.
- Proper model of memory allocation and its initialization on the size of verifiers. For example we definitely need to allocate and initialize structures recursively.
- Separate header file for EMG with implemented interface for memory allocation and initialization.
- Priority changed from Normal to High
Basic C types should be initialized with corresponding nondet functions.
See SV-COMP description:
_VERIFIER_nondet_X(): In order to model nondeterministic values, the following functions can be assumed to return an arbitrary value of the indicated type: __VERIFIER_nondet_X() (and nondet_X(), deprecated) with X in {bool, char, int, float, double, loff_t, long, pchar, pointer, pthread_t, sector_t, short, size_t, u32, uchar, uint, ulong, unsigned, ushort} (no side effects, pointer for void *, etc.).
- Priority changed from High to Normal
Currently EMG uses '__VERIFIER_nondet_pointer()' for initialization of all pointers required for an environment model. Actually it calls function 'ldvemg_undef_ptr' function implemented in 'sv-comp.h' in job presets. The function still has a size parameter but to avoid the problem with incomplete types EMG set it to a senseless constant, so you can implement your own implementation but the size cannot be provided until the problem with incomplete types is solved.
- Status changed from New to Open
Also available in: Atom
PDF