WIP: Proper handling of thread information in witness linter

[SvenUmbricht]

Last year there were several threading-related issues with the linter which raised questions about the witness specification (cf. #30, #33, #36). This PR is to fix the handling of threading-related information in the linter.

[SvenUmbricht]

Even after the changes made in this PR check_function_stack still had some implicit assumptions about the witness that are not enforced by the specification and while trying to fix these I noticed some other issues / underspecifications that have to be resolved before this can be merged:

• What if no thread id is specified on a given edge? A previous version of the specification stated

  If no threadId is given, any thread can be active

  but this line has been removed in 232349268b63886b8955a66e96b143127c8554b4. The current state of this PR is to treat edges without a thread id as if the id of the main thread was specified.

• How to interpret edges having data elements with both enterFunction and returnFromFunction keys? When checking callstack validity the linter assumes function returns to happen first, because otherwise a transition with different values for enterFunction and returnFromFunction would always be invalid.