[x] Must be thoroughly checked by someone before merging, because the last bit was quite difficult and can likely contain mistakes
[x] Revealed some bug: test 02/34 builtin_va_list fails and has to be looked into, ~something to do with the autotuner~:
Fatal error: exception LibraryDsl.Pattern.Expected("Library function is called with more arguments than expected.")
Raised at LibraryDsl.Pattern.fail in file "src/util/library/libraryDsl.ml", line 14, characters 15-33
Called from Goblint_lib__AutoTune.hasFunction.relevant_static.(fun) in file "src/autoTune.ml", line 158, characters 41-60
Called from Stdlib__Map.Make.exists in file "map.ml", line 329, characters 29-34
Called from Goblint_lib__AutoTune.hasFunction in file "src/autoTune.ml", line 175, characters 2-77
Called from Goblint_lib__AutoTune.activateLongjmpAnalysesWhenRequired in file "src/autoTune.ml", line 210, characters 5-26
Called from Dune__exe__Goblint.main in file "src/goblint.ml", line 59, characters 6-53
Called from Stdlib.at_exit.new_exit in file "stdlib.ml", line 560, characters 59-63
Called from Stdlib.do_at_exit in file "stdlib.ml" (inlined), line 566, characters 20-61
Called from Std_exit in file "std_exit.ml", line 18, characters 8-20
See result/index.xml
The latter was caused by the fact that cil has special cases for handling va_arg and va_start functions. Thus, I fixed their argument definitions according to what is written in CIL and left comments.
02/34 builtin_va_listfails and has to be looked into, ~something to do with the autotuner~:The latter was caused by the fact that cil has special cases for handling
va_argandva_startfunctions. Thus, I fixed their argument definitions according to what is written in CIL and left comments.