Skip to content

CONTRATCS: force success for some pointer predicates

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