Skip to content

Commit 09b2fe0

Browse files
committed
Disable a number of invariants that currently fail
This takes us back to the behaviour prior to this series of commits, and effectively is a to-do list to be addressed. We should either handle the cases, or get rid of the instruction type.
1 parent 817fbd2 commit 09b2fe0

5 files changed

+16
-0
lines changed

src/analyses/escape_analysis.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -272,7 +272,9 @@ void escape_domaint::transform(
272272
case SKIP: // No action required
273273
break;
274274
case OTHER:
275+
#if 0
275276
DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
277+
#endif
276278
break;
277279
case INCOMPLETE_GOTO:
278280
case NO_INSTRUCTION_TYPE:

src/analyses/interval_domain.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -125,7 +125,9 @@ void interval_domaint::transform(
125125
case SKIP: // No action required
126126
break;
127127
case OTHER:
128+
#if 0
128129
DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
130+
#endif
129131
break;
130132
case INCOMPLETE_GOTO:
131133
case NO_INSTRUCTION_TYPE:

src/analyses/local_bitvector_analysis.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -313,8 +313,10 @@ void local_bitvector_analysist::build()
313313
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
314314
break;
315315
case RETURN:
316+
#if 0
316317
DATA_INVARIANT(false, "Returns must be removed before analysis");
317318
break;
319+
#endif
318320
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
319321
case ATOMIC_END: // Ignoring is a valid over-approximation
320322
case LOCATION: // No action required
@@ -327,8 +329,10 @@ void local_bitvector_analysist::build()
327329
case END_FUNCTION: // No action required
328330
break;
329331
case OTHER:
332+
#if 0
330333
DATA_INVARIANT(
331334
false, "Unclear what is a safe over-approximation of OTHER");
335+
#endif
332336
break;
333337
case INCOMPLETE_GOTO:
334338
case NO_INSTRUCTION_TYPE:

src/analyses/local_may_alias.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -422,7 +422,9 @@ void local_may_aliast::build(const goto_functiont &goto_function)
422422
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
423423
break;
424424
case RETURN:
425+
#if 0
425426
DATA_INVARIANT(false, "Returns must be removed before analysis");
427+
#endif
426428
break;
427429
case GOTO: // Ignoring the guard is a valid over-approximation
428430
case START_THREAD: // Require a concurrent analysis at higher level
@@ -436,8 +438,10 @@ void local_may_aliast::build(const goto_functiont &goto_function)
436438
case ASSUME: // Ignoring is a valid over-approximation
437439
break;
438440
case OTHER:
441+
#if 0
439442
DATA_INVARIANT(
440443
false, "Unclear what is a safe over-approximation of OTHER");
444+
#endif
441445
break;
442446
case INCOMPLETE_GOTO:
443447
case NO_INSTRUCTION_TYPE:

src/analyses/uncaught_exceptions_analysis.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,9 @@ void uncaught_exceptions_domaint::transform(
130130
case ASSIGN: // Safe to ignore in this context
131131
break;
132132
case RETURN:
133+
#if 0
133134
DATA_INVARIANT(false, "Returns must be removed before analysis");
135+
#endif
134136
break;
135137
case GOTO: // Ignoring the guard is a valid over-approximation
136138
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
@@ -144,7 +146,9 @@ void uncaught_exceptions_domaint::transform(
144146
case SKIP: // No action required
145147
break;
146148
case OTHER:
149+
#if 0
147150
DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
151+
#endif
148152
break;
149153
case INCOMPLETE_GOTO:
150154
case NO_INSTRUCTION_TYPE:

0 commit comments

Comments
 (0)