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

Introduce floatbv_round_to_integral_exprt #8538

Open
wants to merge 2 commits into
base: develop
Choose a base branch
from

Introduce floatbv_round_to_integral_exprt

ddeedbc
Select commit
Loading
Failed to load commit list.
Open

Introduce floatbv_round_to_integral_exprt #8538

Introduce floatbv_round_to_integral_exprt
ddeedbc
Select commit
Loading
Failed to load commit list.
Codecov / codecov/patch succeeded Jan 10, 2025 in 1s

78.89% of diff hit (target 78.79%)

View this Pull Request on Codecov

78.89% of diff hit (target 78.79%)

Annotations

Check warning on line 2195 in jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp#L2195 

Added line #L2195 was not covered by tests

Check warning on line 291 in src/analyses/interval_domain.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/analyses/interval_domain.cpp#L291 

Added line #L291 was not covered by tests

Check warning on line 316 in src/analyses/interval_domain.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/analyses/interval_domain.cpp#L316 

Added line #L316 was not covered by tests

Check warning on line 3249 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#L3247-L3249 

Added lines #L3247 - L3249 were not covered by tests

Check warning on line 765 in src/ansi-c/goto-conversion/goto_check_c.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/ansi-c/goto-conversion/goto_check_c.cpp#L764-L765 

Added lines #L764 - L765 were not covered by tests

Check warning on line 770 in src/ansi-c/goto-conversion/goto_check_c.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/ansi-c/goto-conversion/goto_check_c.cpp#L770 

Added line #L770 was not covered by tests

Check warning on line 849 in src/ansi-c/goto-conversion/goto_check_c.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/ansi-c/goto-conversion/goto_check_c.cpp#L848-L849 

Added lines #L848 - L849 were not covered by tests

Check warning on line 854 in src/ansi-c/goto-conversion/goto_check_c.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/ansi-c/goto-conversion/goto_check_c.cpp#L854 

Added line #L854 was not covered by tests

Check warning on line 74 in src/ansi-c/literals/convert_float_literal.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/ansi-c/literals/convert_float_literal.cpp#L74 

Added line #L74 was not covered by tests

Check warning on line 579 in src/goto-programs/interpreter.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-programs/interpreter.cpp#L579 

Added line #L579 was not covered by tests

Check warning on line 367 in src/goto-programs/interpreter_evaluate.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-programs/interpreter_evaluate.cpp#L367 

Added line #L367 was not covered by tests

Check warning on line 736 in src/goto-programs/interpreter_evaluate.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/goto-programs/interpreter_evaluate.cpp#L734-L736 

Added lines #L734 - L736 were not covered by tests

Check warning on line 98 in src/solvers/flattening/boolbv_floatbv_op.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/solvers/flattening/boolbv_floatbv_op.cpp#L98 

Added line #L98 was not covered by tests

Check warning on line 155 in src/solvers/floatbv/float_utils.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/solvers/floatbv/float_utils.cpp#L155 

Added line #L155 was not covered by tests

Check warning on line 159 in src/solvers/floatbv/float_utils.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/solvers/floatbv/float_utils.cpp#L159 

Added line #L159 was not covered by tests

Check warning on line 161 in src/solvers/floatbv/float_utils.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/solvers/floatbv/float_utils.cpp#L161 

Added line #L161 was not covered by tests

Check warning on line 164 in src/solvers/floatbv/float_utils.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/solvers/floatbv/float_utils.cpp#L164 

Added line #L164 was not covered by tests

Check warning on line 166 in src/solvers/floatbv/float_utils.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/solvers/floatbv/float_utils.cpp#L166 

Added line #L166 was not covered by tests

Check warning on line 169 in src/solvers/floatbv/float_utils.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/solvers/floatbv/float_utils.cpp#L169 

Added line #L169 was not covered by tests

Check warning on line 171 in src/solvers/floatbv/float_utils.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/solvers/floatbv/float_utils.cpp#L171 

Added line #L171 was not covered by tests

Check warning on line 173 in src/solvers/floatbv/float_utils.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/solvers/floatbv/float_utils.cpp#L173 

Added line #L173 was not covered by tests

Check warning on line 176 in src/solvers/floatbv/float_utils.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/solvers/floatbv/float_utils.cpp#L175-L176 

Added lines #L175 - L176 were not covered by tests

Check warning on line 1206 in src/solvers/smt2/smt2_conv.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L1206 

Added line #L1206 was not covered by tests

Check warning on line 3282 in src/solvers/smt2/smt2_conv.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L3281-L3282 

Added lines #L3281 - L3282 were not covered by tests

Check warning on line 3284 in src/solvers/smt2/smt2_conv.cpp

See this annotation in the file changed.

@codecov codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L3284 

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