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

CONTRATCS: force success for necessary pointer predicates #8574

Merged
merged 1 commit into from
Jan 24, 2025

CONTRATCS: force success for some pointer predicates

3ddd4b6
Select commit
Loading
Failed to load commit list.
Merged

CONTRATCS: force success for necessary pointer predicates #8574

CONTRATCS: force success for some pointer predicates
3ddd4b6
Select commit
Loading
Failed to load commit list.
Codecov / codecov/patch failed Jan 24, 2025 in 1s

46.46% of diff hit (target 78.94%)

View this Pull Request on Codecov

46.46% of diff hit (target 78.94%)

Annotations

Check warning on line 65 in src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp#L65 

Added line #L65 was not covered by tests

Check warning on line 91 in src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp#L91 

Added line #L91 was not covered by tests

Check warning on line 95 in src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp#L94-L95 

Added lines #L94 - L95 were not covered by tests

Check warning on line 75 in src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp#L75 

Added line #L75 was not covered by tests

Check warning on line 77 in src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp#L77 

Added line #L77 was not covered by tests

Check warning on line 118 in src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp#L117-L118 

Added lines #L117 - L118 were not covered by tests

Check warning on line 59 in src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp#L59 

Added line #L59 was not covered by tests

Check warning on line 74 in src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp#L74 

Added line #L74 was not covered by tests

Check warning on line 543 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L543 

Added line #L543 was not covered by tests

Check warning on line 545 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L545 

Added line #L545 was not covered by tests

Check warning on line 556 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L547-L556 

Added lines #L547 - L556 were not covered by tests

Check warning on line 558 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L558 

Added line #L558 was not covered by tests

Check warning on line 564 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L560-L564 

Added lines #L560 - L564 were not covered by tests

Check warning on line 568 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L568 

Added line #L568 was not covered by tests

Check warning on line 570 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L570 

Added line #L570 was not covered by tests

Check warning on line 576 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L575-L576 

Added lines #L575 - L576 were not covered by tests

Check warning on line 579 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L579 

Added line #L579 was not covered by tests

Check warning on line 582 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L582 

Added line #L582 was not covered by tests

Check warning on line 585 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L585 

Added line #L585 was not covered by tests

Check warning on line 594 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L593-L594 

Added lines #L593 - L594 were not covered by tests

Check warning on line 596 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L596 

Added line #L596 was not covered by tests

Check warning on line 602 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L602 

Added line #L602 was not covered by tests

Check warning on line 604 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L604 

Added line #L604 was not covered by tests

Check warning on line 609 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L609 

Added line #L609 was not covered by tests

Check warning on line 611 in src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp#L611 

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