-
Notifications
You must be signed in to change notification settings - Fork 277
Description
CBMC version: 5.62.0
Operating system: macOS 11.6.6
Exact command line resulting in the issue:
Any flow that checks or abstracts function contracts. For example,
goto-instrument --enforce-contract coverage_abstraction_add_ten coverage_abstraction_add_ten_harness.c8.goto coverage_abstraction_add_ten_harness.c9.goto
Here is an example using the CBMC Starter Kit (let me know if repository is inaccessible):
https://github.com/nwetzler/cbmc-test/tree/main/proofs/coverage_abstraction_add_ten
What behaviour did you expect:
Expected behavior is that all instrumented code for function contracts should include a file, line number, and function name.
What happened instead:
Function names are missing from instrumented GOTO statements. See the example below:
// 8 file coverage_abstraction.c line 4
DECL goto_convertt::tmp_if_expr$0 : 𝔹
// 9 file coverage_abstraction.c line 4
IF ¬(coverage_abstraction_add_ten::tmp_cc ≠ NULL) THEN GOTO 3
// 10 file coverage_abstraction.c line 5
DECL goto_convertt::tmp_if_expr : 𝔹
// 11 file coverage_abstraction.c line 5
IF ¬(0 ≤ *coverage_abstraction_add_ten::tmp_cc) THEN GOTO 1