File tree 5 files changed +18
-0
lines changed
5 files changed +18
-0
lines changed Original file line number Diff line number Diff line change @@ -272,7 +272,9 @@ void escape_domaint::transform(
272
272
case SKIP: // No action required
273
273
break ;
274
274
case OTHER:
275
+ #if 0
275
276
DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
277
+ #endif
276
278
break ;
277
279
case INCOMPLETE_GOTO:
278
280
case NO_INSTRUCTION_TYPE:
Original file line number Diff line number Diff line change @@ -125,7 +125,9 @@ void interval_domaint::transform(
125
125
case SKIP: // No action required
126
126
break ;
127
127
case OTHER:
128
+ #if 0
128
129
DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
130
+ #endif
129
131
break ;
130
132
case INCOMPLETE_GOTO:
131
133
case NO_INSTRUCTION_TYPE:
Original file line number Diff line number Diff line change @@ -310,11 +310,15 @@ void local_bitvector_analysist::build()
310
310
311
311
case CATCH:
312
312
case THROW:
313
+ #if 0
313
314
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
314
315
break;
316
+ #endif
315
317
case RETURN:
318
+ #if 0
316
319
DATA_INVARIANT(false, "Returns must be removed before analysis");
317
320
break;
321
+ #endif
318
322
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
319
323
case ATOMIC_END: // Ignoring is a valid over-approximation
320
324
case LOCATION: // No action required
@@ -327,8 +331,10 @@ void local_bitvector_analysist::build()
327
331
case END_FUNCTION: // No action required
328
332
break ;
329
333
case OTHER:
334
+ #if 0
330
335
DATA_INVARIANT(
331
336
false, "Unclear what is a safe over-approximation of OTHER");
337
+ #endif
332
338
break ;
333
339
case INCOMPLETE_GOTO:
334
340
case NO_INSTRUCTION_TYPE:
Original file line number Diff line number Diff line change @@ -422,7 +422,9 @@ void local_may_aliast::build(const goto_functiont &goto_function)
422
422
DATA_INVARIANT (false , " Exceptions must be removed before analysis" );
423
423
break ;
424
424
case RETURN:
425
+ #if 0
425
426
DATA_INVARIANT(false, "Returns must be removed before analysis");
427
+ #endif
426
428
break ;
427
429
case GOTO: // Ignoring the guard is a valid over-approximation
428
430
case START_THREAD: // Require a concurrent analysis at higher level
@@ -436,8 +438,10 @@ void local_may_aliast::build(const goto_functiont &goto_function)
436
438
case ASSUME: // Ignoring is a valid over-approximation
437
439
break ;
438
440
case OTHER:
441
+ #if 0
439
442
DATA_INVARIANT(
440
443
false, "Unclear what is a safe over-approximation of OTHER");
444
+ #endif
441
445
break ;
442
446
case INCOMPLETE_GOTO:
443
447
case NO_INSTRUCTION_TYPE:
Original file line number Diff line number Diff line change @@ -130,7 +130,9 @@ void uncaught_exceptions_domaint::transform(
130
130
case ASSIGN: // Safe to ignore in this context
131
131
break ;
132
132
case RETURN:
133
+ #if 0
133
134
DATA_INVARIANT(false, "Returns must be removed before analysis");
135
+ #endif
134
136
break ;
135
137
case GOTO: // Ignoring the guard is a valid over-approximation
136
138
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
@@ -144,7 +146,9 @@ void uncaught_exceptions_domaint::transform(
144
146
case SKIP: // No action required
145
147
break ;
146
148
case OTHER:
149
+ #if 0
147
150
DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
151
+ #endif
148
152
break ;
149
153
case INCOMPLETE_GOTO:
150
154
case NO_INSTRUCTION_TYPE:
You can’t perform that action at this time.
0 commit comments