Skip to content

Add new `__CPROVER_pointer_equals(p, q)` predicate

Codecov / codecov/patch failed Jan 21, 2025 in 0s

59.57% of diff hit (target 78.95%)

View this Pull Request on Codecov

59.57% of diff hit (target 78.95%)

Annotations

Check warning on line 2601 in src/ansi-c/c_typecheck_expr.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/ansi-c/c_typecheck_expr.cpp#L2598-L2601 

Added lines #L2598 - L2601 were not covered by tests

Check warning on line 49 in src/ansi-c/cprover_library.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/ansi-c/cprover_library.cpp#L49 

Added line #L49 was not covered by tests

Check warning on line 53 in src/ansi-c/cprover_library.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/ansi-c/cprover_library.cpp#L52-L53 

Added lines #L52 - L53 were not covered by tests

Check warning on line 241 in src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp#L241 

Added line #L241 was not covered by tests

Check warning on line 244 in src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp#L244 

Added line #L244 was not covered by tests

Check warning on line 31 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#L31 

Added line #L31 was not covered by tests

Check warning on line 35 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#L35 

Added line #L35 was not covered by tests

Check warning on line 38 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#L38 

Added line #L38 was not covered by tests

Check warning on line 40 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#L40 

Added line #L40 was not covered by tests

Check warning on line 79 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#L79 

Added line #L79 was not covered by tests

Check warning on line 102 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#L102 

Added line #L102 was not covered by tests

Check warning on line 107 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#L104-L107 

Added lines #L104 - L107 were not covered by tests

Check warning on line 109 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#L109 

Added line #L109 was not covered by tests

Check warning on line 113 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#L113 

Added line #L113 was not covered by tests

Check warning on line 117 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 

Added line #L117 was not covered by tests

Check warning on line 121 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#L120-L121 

Added lines #L120 - L121 were not covered by tests

Check warning on line 124 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#L123-L124 

Added lines #L123 - L124 were not covered by tests

Check warning on line 127 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#L127 

Added line #L127 was not covered by tests

Check warning on line 130 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#L130 

Added line #L130 was not covered by tests

Check warning on line 132 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#L132 

Added line #L132 was not covered by tests

Check warning on line 136 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#L136 

Added line #L136 was not covered by tests

Check warning on line 138 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#L138 

Added line #L138 was not covered by tests

Check warning on line 141 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#L141 

Added line #L141 was not covered by tests

Check warning on line 145 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#L144-L145 

Added lines #L144 - L145 were not covered by tests

Check warning on line 1168 in src/util/config.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/util/config.cpp#L1168 

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