-
Notifications
You must be signed in to change notification settings - Fork 169
Undefined behavior with function pointers in heap-manipulation/dll_of_dll* #462
Comments
Ok, I forgot that I think there is something missing in the C standard for this case, because the standard only declares that calling a function via an incompatible function-pointer is undefined, but function-pointers with unspecified parameter lists are compatible to all other function pointers with the same return type. I don't see anything that forbids taking the address of a function with signature Furthermore, using an empty parameter list in a function pointer is declared as "obsolescent" by the C standard in 6.11.6 and should not be used in new programs. So we might still want to change this code. |
heap-manipulation: resolve function pointer with unspecified arguments (#462)
Should be resolved by pull request #483 . |
Based on Linux drivers Fix sanity checks Remove copy-pasted flag The suppress_warnings flag is not neccesary Disable particular warnings of CLANG Minor change: remove comments Fix problems with uninitizized variables Minor changes Add instructions for obtaining the benchmarks Extract pthread-specific code into header file Add stubs for all undefined functions Update documentation on how to submit verification tasks. - Move checklist for PRs to a PR template that GitHub will insert automatically in the description field for new PRs. - Document everything that submitters should read in new file CONTRIBUTING.md, for which GitHub will automatically show a link when creating a new issue or PR. - Remove content that is now in CONTRIBUTING.md from README.md. Fixes sosy-lab#167. use full links in PR template because otherwise links are broken Adding a template for verification tasks, and a new template-set file Add sanity checks for duplicate and contradicting properties Fix bug in check.py that did not check for unknown violated properties Adapt our varios check scripts to the new directories and files Restructure and adjust headings Add links to defining secions The text should not be SV-COMP specific. More on parameters Describe the templates for verification tasks Description and motivation of the repository Added property 'memcleanup' Benchmarks for testing operations on sets Make list implementation of sets Fix other examples Add Makefile Add preprocessed files Add sets to ReachSafety-Heap Add license Add Readme use 'cpp -P' for preprocessing Move aux files to model dir Replace license file by symlink Ignore model dir Enable warnings Add empty Makefile (the model dir is ignored) Suppress 'unexpected subdirectory model' for ldv-sets Disable warnings about incompatible redeclaration of library functions Not required use -m32 for preprocessing Add contributed by Add test for unbounded case Remove cillified files from repository for which we have corresponding non-cillified files. These were removed from the actual benchmark sets 4 years ago in 4f80d53. Remove duplicate files. This fixes most of sosy-lab#445 according to the explanation from sosy-lab#445 (comment) Remove another duplicate file and ajust some filenames as suggested by sosy-lab#445 (comment) Remove one of each of the remaining duplicate file pairs (picked arbitrarily) Fix undefined behavior in volatile_alias.c There was an assignment of the address of a volatile int to an int* pointer, loosing the volatile modifier. To keep the original intention of the benchmark, there is now an assignment of the address of an int to a volatile int*. Rename property to positive name Rename categories with property NoOverflow to positive name Fix link in README for renamed property heap-manipulation: resolve function pointer with unspecified arguments (sosy-lab#462) (*insert_fnc)() declares insert_fnc as a function pointer with an unknown number and type of parameters, not with an empty list of parameters. This may be an underspecification that can lead to possible undefined behaviour. This commit fixes that in two benchmarks of Predator. heap_manipulation: commit also *.i files heap-manipulation: fix problems with fnc pointers heap-manipulation: fix *.i files heap-manipulation: re-pre-process with -m32 Add model directory Exclude model directory from building process
The
heap-manipulation/dll_of_dll*
files (e.g., this one) have a functiondll_create_generic
that accepts a function pointer of typevoid (*insert_fnc)()
, i.e., the function pointer takes no arguments. However, when callinginsert_fnc
, an argument is passed, and indeed, the functions that are called at runtime throughinsert_fnc
(dll_insert_master
anddll_insert_slave
) require a parameter. This is undefined behavior (explanation with links to C standard).For full standard compatibility, we need to change the function pointer to take an argument of type
void **
, and we need to changedll_insert_master
anddll_insert_slave
to also acceptvoid **
and do a cast inside these functions. Everything else is undefined behavior. In practice, however, I suspect there exists a lot of code that expects that it works if we only add thevoid **
argument to the function pointer, without changing the signature ofdll_insert_master
anddll_insert_slave
. What do we want to do here?The text was updated successfully, but these errors were encountered: