Bug #6574
openInitialize callback parameters by default
0%
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.
Updated by Evgeny Novikov over 8 years ago
- Subject changed from Initialize defualt values to Initialize default values
- Description updated (diff)
I dislike "default values". Maybe "callback parameters" would be better.
Updated by Ilja Zakharov over 8 years ago
- Subject changed from Initialize default values to Initialize callback parameters by default
Updated by Ilja Zakharov over 8 years ago
- 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.
Updated by Vadim Mutilin over 8 years ago
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.).
Updated by Ilja Zakharov over 8 years ago
- 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.