Taclet definition added to problemHeader

[wadoon]

Related Issue

This pull request resolves #849 .

Intended Change

Compute a proper problem header including also the taclets and all other definitions.

The problem header is delivered through the initConfig, which may be problematic.

Plan

• fixing it

Type of pull request

• Bug fix (non-breaking change which fixes an issue)

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
  IT IS TOO LATE FOR JAVADOC *yawn*

• I have tested the feature as follows: by hand

[unp1]

Thanks. At the moment I get exception when saving aproof that was started not via a .key file but by selecting a directory and choosing a proof obligation.

Steps to reproduce:

• File > Open:
  • Navigate to examples/firstTouch/06-BinarySearch
  • Select the src/ folder
• Run the proof
• Saving the completed proof results in the error message "No proof present"

[wadoon]

Thanks. At the moment I get exception when saving aproof that was started not via a .key file but by selecting a directory and choosing a proof obligation.

Should be resolved. NPE during saving as the header variable is null, as these proofs are not obtained by reading a KeY-file.

[unp1]

Should be resolved. NPE during saving as the header variable is null, as these proofs are not obtained by reading a KeY-file.

Thanks. I can save the proof now, but reloading gives me the error:
BinarySearch[BinarySearch::search([I,int)].JML normal_behavior operation contract.0

[unp1]

Problem:

1. Load examples/heap/saddleback_search/Saddleback.java directly (not via a .key file)
2. Do some proof steps
3. Save proof
4. Loading proof fails

[wadoon]

Problem:

1. Load examples/heap/saddleback_search/Saddleback.java directly (not via a .key file)
2. Do some proof steps
3. Save proof
4. Loading proof fails

repaired.