Skip to content

Commit 52c3dbb

Browse files
tautschnigtautschnig
authored
Merge pull request #8297 from diffblue/goto-check-c-fatal
`goto_check_ct::add_guarded_property` now has `is_fatal` parameter
2 parents 6b44128 + 5c5895b commit 52c3dbb

File tree

1 file changed

+43
-1
lines changed

1 file changed

+43
-1
lines changed

Diff for: ‎src/ansi-c/goto-conversion/goto_check_c.cpp

+43-1
Original file line numberDiff line numberDiff line change
@@ -237,6 +237,7 @@ class goto_check_ct
237237
/// \param asserted_expr: expression to be asserted
238238
/// \param comment: human readable comment
239239
/// \param property_class: classification of the property
240+
/// \param is_fatal: property checks for undefined behavior
240241
/// \param source_location: the source location of the original expression
241242
/// \param src_expr: the original expression to be included in the comment
242243
/// \param guard: the condition under which the asserted expression should be
@@ -245,6 +246,7 @@ class goto_check_ct
245246
const exprt &asserted_expr,
246247
const std::string &comment,
247248
const std::string &property_class,
249+
bool is_fatal,
248250
const source_locationt &source_location,
249251
const exprt &src_expr,
250252
const guardt &guard);
@@ -507,6 +509,7 @@ void goto_check_ct::div_by_zero_check(
507509
inequality,
508510
"division by zero",
509511
"division-by-zero",
512+
true, // fatal
510513
expr.find_source_location(),
511514
expr,
512515
guard);
@@ -528,6 +531,7 @@ void goto_check_ct::float_div_by_zero_check(
528531
inequality,
529532
"floating-point division by zero",
530533
"float-division-by-zero",
534+
false, // fatal
531535
expr.find_source_location(),
532536
expr,
533537
guard);
@@ -552,6 +556,7 @@ void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard)
552556
check,
553557
"enum range check",
554558
"enum-range-check",
559+
false, // fatal
555560
expr.find_source_location(),
556561
expr,
557562
guard);
@@ -578,6 +583,7 @@ void goto_check_ct::undefined_shift_check(
578583
inequality,
579584
"shift distance is negative",
580585
"undefined-shift",
586+
false, // fatal
581587
expr.find_source_location(),
582588
expr,
583589
guard);
@@ -594,6 +600,7 @@ void goto_check_ct::undefined_shift_check(
594600
binary_relation_exprt(expr.distance(), ID_lt, std::move(width_expr)),
595601
"shift distance too large",
596602
"undefined-shift",
603+
false, // fatal
597604
expr.find_source_location(),
598605
expr,
599606
guard);
@@ -607,6 +614,7 @@ void goto_check_ct::undefined_shift_check(
607614
inequality,
608615
"shift operand is negative",
609616
"undefined-shift",
617+
false, // fatal
610618
expr.find_source_location(),
611619
expr,
612620
guard);
@@ -618,6 +626,7 @@ void goto_check_ct::undefined_shift_check(
618626
false_exprt(),
619627
"shift of non-integer type",
620628
"undefined-shift",
629+
false, // fatal
621630
expr.find_source_location(),
622631
expr,
623632
guard);
@@ -640,6 +649,7 @@ void goto_check_ct::mod_by_zero_check(
640649
inequality,
641650
"division by zero",
642651
"division-by-zero",
652+
false, // fatal
643653
expr.find_source_location(),
644654
expr,
645655
guard);
@@ -672,6 +682,7 @@ void goto_check_ct::mod_overflow_check(
672682
or_exprt(int_min_neq, minus_one_neq),
673683
"result of signed mod is not representable",
674684
"overflow",
685+
false, // fatal
675686
expr.find_source_location(),
676687
expr,
677688
guard);
@@ -716,6 +727,7 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
716727
and_exprt(no_overflow_lower, no_overflow_upper),
717728
"arithmetic overflow on signed type conversion",
718729
"overflow",
730+
false, // fatal
719731
expr.find_source_location(),
720732
expr,
721733
guard);
@@ -733,6 +745,7 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
733745
no_overflow_upper,
734746
"arithmetic overflow on unsigned to signed type conversion",
735747
"overflow",
748+
false, // fatal
736749
expr.find_source_location(),
737750
expr,
738751
guard);
@@ -754,6 +767,7 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
754767
and_exprt(no_overflow_lower, no_overflow_upper),
755768
"arithmetic overflow on float to signed integer type conversion",
756769
"overflow",
770+
false, // fatal
757771
expr.find_source_location(),
758772
expr,
759773
guard);
@@ -777,6 +791,7 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
777791
no_overflow_lower,
778792
"arithmetic overflow on signed to unsigned type conversion",
779793
"overflow",
794+
false, // fatal
780795
expr.find_source_location(),
781796
expr,
782797
guard);
@@ -794,6 +809,7 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
794809
and_exprt(no_overflow_lower, no_overflow_upper),
795810
"arithmetic overflow on signed to unsigned type conversion",
796811
"overflow",
812+
false, // fatal
797813
expr.find_source_location(),
798814
expr,
799815
guard);
@@ -812,6 +828,7 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
812828
no_overflow_upper,
813829
"arithmetic overflow on unsigned to unsigned type conversion",
814830
"overflow",
831+
false, // fatal
815832
expr.find_source_location(),
816833
expr,
817834
guard);
@@ -833,6 +850,7 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
833850
and_exprt(no_overflow_lower, no_overflow_upper),
834851
"arithmetic overflow on float to unsigned integer type conversion",
835852
"overflow",
853+
false, // fatal
836854
expr.find_source_location(),
837855
expr,
838856
guard);
@@ -875,6 +893,7 @@ void goto_check_ct::integer_overflow_check(
875893
not_exprt(and_exprt(int_min_eq, minus_one_eq)),
876894
"arithmetic overflow on signed division",
877895
"overflow",
896+
false, // fatal
878897
expr.find_source_location(),
879898
expr,
880899
guard);
@@ -896,6 +915,7 @@ void goto_check_ct::integer_overflow_check(
896915
not_exprt(int_min_eq),
897916
"arithmetic overflow on signed unary minus",
898917
"overflow",
918+
false, // fatal
899919
expr.find_source_location(),
900920
expr,
901921
guard);
@@ -912,6 +932,7 @@ void goto_check_ct::integer_overflow_check(
912932
not_eq_zero,
913933
"arithmetic overflow on unsigned unary minus",
914934
"overflow",
935+
false, // fatal
915936
expr.find_source_location(),
916937
expr,
917938
guard);
@@ -1018,6 +1039,7 @@ void goto_check_ct::integer_overflow_check(
10181039
top_bits_zero}),
10191040
"arithmetic overflow on signed shl",
10201041
"overflow",
1042+
false, // fatal
10211043
expr.find_source_location(),
10221044
expr,
10231045
guard);
@@ -1052,6 +1074,7 @@ void goto_check_ct::integer_overflow_check(
10521074
not_exprt{binary_overflow_exprt{tmp, expr.id(), expr.operands()[i]}},
10531075
"arithmetic overflow on " + kind + " " + expr.id_string(),
10541076
"overflow",
1077+
false, // fatal
10551078
expr.find_source_location(),
10561079
expr,
10571080
guard);
@@ -1066,6 +1089,7 @@ void goto_check_ct::integer_overflow_check(
10661089
not_exprt{binary_overflow_exprt{bexpr.lhs(), expr.id(), bexpr.rhs()}},
10671090
"arithmetic overflow on " + kind + " " + expr.id_string(),
10681091
"overflow",
1092+
false, // fatal
10691093
expr.find_source_location(),
10701094
expr,
10711095
guard);
@@ -1080,6 +1104,7 @@ void goto_check_ct::integer_overflow_check(
10801104
not_exprt{unary_minus_overflow_exprt{to_unary_expr(expr).op()}},
10811105
"arithmetic overflow on " + kind + " " + expr.id_string(),
10821106
"overflow",
1107+
false, // fatal
10831108
expr.find_source_location(),
10841109
expr,
10851110
guard);
@@ -1113,6 +1138,7 @@ void goto_check_ct::float_overflow_check(const exprt &expr, const guardt &guard)
11131138
std::move(overflow_check),
11141139
"arithmetic overflow on floating-point typecast",
11151140
"overflow",
1141+
false, // fatal
11161142
expr.find_source_location(),
11171143
expr,
11181144
guard);
@@ -1124,6 +1150,7 @@ void goto_check_ct::float_overflow_check(const exprt &expr, const guardt &guard)
11241150
not_exprt(isinf_exprt(expr)),
11251151
"arithmetic overflow on floating-point typecast",
11261152
"overflow",
1153+
false, // fatal
11271154
expr.find_source_location(),
11281155
expr,
11291156
guard);
@@ -1141,6 +1168,7 @@ void goto_check_ct::float_overflow_check(const exprt &expr, const guardt &guard)
11411168
std::move(overflow_check),
11421169
"arithmetic overflow on floating-point division",
11431170
"overflow",
1171+
false, // fatal
11441172
expr.find_source_location(),
11451173
expr,
11461174
guard);
@@ -1176,6 +1204,7 @@ void goto_check_ct::float_overflow_check(const exprt &expr, const guardt &guard)
11761204
std::move(overflow_check),
11771205
"arithmetic overflow on floating-point " + kind,
11781206
"overflow",
1207+
false, // fatal
11791208
expr.find_source_location(),
11801209
expr,
11811210
guard);
@@ -1296,6 +1325,7 @@ void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
12961325
boolean_negate(isnan),
12971326
"NaN on " + expr.id_string(),
12981327
"NaN",
1328+
false, // fatal
12991329
expr.find_source_location(),
13001330
expr,
13011331
guard);
@@ -1320,6 +1350,7 @@ void goto_check_ct::pointer_rel_check(
13201350
same_object,
13211351
"same object violation",
13221352
"pointer",
1353+
false, // fatal
13231354
expr.find_source_location(),
13241355
expr,
13251356
guard);
@@ -1337,6 +1368,7 @@ void goto_check_ct::pointer_rel_check(
13371368
c.assertion,
13381369
"pointer relation: " + c.description,
13391370
"pointer arithmetic",
1371+
false, // fatal
13401372
expr.find_source_location(),
13411373
pointer,
13421374
guard);
@@ -1395,6 +1427,7 @@ void goto_check_ct::pointer_overflow_check(
13951427
c.assertion,
13961428
"pointer arithmetic: " + c.description,
13971429
"pointer arithmetic",
1430+
false, // fatal
13981431
expr.find_source_location(),
13991432
expr,
14001433
guard);
@@ -1436,6 +1469,7 @@ void goto_check_ct::pointer_validity_check(
14361469
c.assertion,
14371470
"dereference failure: " + c.description,
14381471
"pointer dereference",
1472+
false, // fatal
14391473
src_expr.find_source_location(),
14401474
src_expr,
14411475
guard);
@@ -1477,6 +1511,7 @@ void goto_check_ct::pointer_primitive_check(
14771511
or_exprt{null_object(pointer), c.assertion},
14781512
c.description,
14791513
"pointer primitives",
1514+
false, // fatal
14801515
expr.source_location(),
14811516
expr,
14821517
guard);
@@ -1593,6 +1628,7 @@ void goto_check_ct::bounds_check_index(
15931628
inequality,
15941629
name + " lower bound",
15951630
"array bounds",
1631+
false, // fatal
15961632
expr.find_source_location(),
15971633
expr,
15981634
guard);
@@ -1627,6 +1663,7 @@ void goto_check_ct::bounds_check_index(
16271663
precond,
16281664
name + " dynamic object upper bound",
16291665
"array bounds",
1666+
false, // fatal
16301667
expr.find_source_location(),
16311668
expr,
16321669
guard);
@@ -1671,6 +1708,7 @@ void goto_check_ct::bounds_check_index(
16711708
inequality,
16721709
name + " upper bound",
16731710
"array bounds",
1711+
false, // fatal
16741712
expr.find_source_location(),
16751713
expr,
16761714
guard);
@@ -1684,6 +1722,7 @@ void goto_check_ct::bounds_check_index(
16841722
inequality,
16851723
name + " upper bound",
16861724
"array bounds",
1725+
false, // fatal
16871726
expr.find_source_location(),
16881727
expr,
16891728
guard);
@@ -1707,6 +1746,7 @@ void goto_check_ct::bounds_check_bit_count(
17071746
notequal_exprt{expr.op(), from_integer(0, expr.op().type())},
17081747
"count " + name + " zeros is undefined for value zero",
17091748
"bit count",
1749+
false, // fatal
17101750
expr.find_source_location(),
17111751
expr,
17121752
guard);
@@ -1716,6 +1756,7 @@ void goto_check_ct::add_guarded_property(
17161756
const exprt &asserted_expr,
17171757
const std::string &comment,
17181758
const std::string &property_class,
1759+
bool is_fatal,
17191760
const source_locationt &source_location,
17201761
const exprt &src_expr,
17211762
const guardt &guard)
@@ -1749,7 +1790,7 @@ void goto_check_ct::add_guarded_property(
17491790
}
17501791
else
17511792
{
1752-
if(property_class == "division-by-zero")
1793+
if(is_fatal)
17531794
annotated_location.property_fatal(true);
17541795

17551796
new_code.add(goto_programt::make_assertion(
@@ -2040,6 +2081,7 @@ void goto_check_ct::memory_leak_check(const irep_idt &function_id)
20402081
eq,
20412082
"dynamically allocated memory never freed",
20422083
"memory-leak",
2084+
false, // fatal
20432085
source_location,
20442086
eq,
20452087
identity);

0 commit comments

Comments
 (0)