Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[CONTRACTS] Check side effect of loop contracts during instrumentation #8360

Merged
merged 1 commit into from
Jul 22, 2024

Check side effect of loop contracts during instrumentation

2d416e1
Select commit
Loading
Failed to load commit list.
Merged

[CONTRACTS] Check side effect of loop contracts during instrumentation #8360

Check side effect of loop contracts during instrumentation
2d416e1
Select commit
Loading
Failed to load commit list.
Codecov / codecov/patch succeeded Jul 22, 2024 in 0s

82.75% of diff hit (target 78.34%)

View this Pull Request on Codecov

82.75% of diff hit (target 78.34%)

Annotations

Check warning on line 34 in src/cprover/instrument_given_invariants.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/cprover/instrument_given_invariants.cpp#L34 

Added line #L34 was not covered by tests

Check warning on line 36 in src/cprover/instrument_given_invariants.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/cprover/instrument_given_invariants.cpp#L36 

Added line #L36 was not covered by tests

Check warning on line 36 in src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp#L36 

Added line #L36 was not covered by tests

Check warning on line 145 in src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp#L143-L145 

Added lines #L143 - L145 were not covered by tests

Check warning on line 422 in src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp#L422 

Added line #L422 was not covered by tests

Check warning on line 442 in src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp#L442 

Added line #L442 was not covered by tests

Check warning on line 715 in src/goto-instrument/contracts/utils.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/utils.cpp#L715 

Added line #L715 was not covered by tests

Check warning on line 717 in src/goto-instrument/contracts/utils.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/utils.cpp#L717 

Added line #L717 was not covered by tests
View more details on Codecov