diff --git a/src/plugins/e-acsl/tests/arith/neg_rte_int.c b/src/plugins/e-acsl/tests/arith/neg_rte_int.c new file mode 100644 index 0000000000000000000000000000000000000000..d31e60b261b9eb6a9e5923f5463578f6918f55af --- /dev/null +++ b/src/plugins/e-acsl/tests/arith/neg_rte_int.c @@ -0,0 +1,11 @@ +/* run.config + STDOPT: #"-rte" + COMMENT: Generates an RTE with a negative integer + COMMENT: (The negative integer being the lower bound of signed chars) + COMMENT: This regression test ensures that E-ACSL correctly handles negative integers. +*/ +char c; +float f; +void main() { + c = f + 0.5; +}