@@ -786,15 +786,20 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const
786
786
switch (type)
787
787
{
788
788
case goto_trace_stept::typet::ASSERT:
789
- out << " ASSERT " << format (cond_expr) << ' \n ' ; break ;
789
+ out << " ASSERT " << format (cond_expr) << ' \n ' ;
790
+ break ;
790
791
case goto_trace_stept::typet::ASSUME:
791
- out << " ASSUME " << format (cond_expr) << ' \n ' ; break ;
792
+ out << " ASSUME " << format (cond_expr) << ' \n ' ;
793
+ break ;
792
794
case goto_trace_stept::typet::LOCATION:
793
- out << " LOCATION" << ' \n ' ; break ;
795
+ out << " LOCATION" << ' \n ' ;
796
+ break ;
794
797
case goto_trace_stept::typet::INPUT:
795
- out << " INPUT" << ' \n ' ; break ;
798
+ out << " INPUT" << ' \n ' ;
799
+ break ;
796
800
case goto_trace_stept::typet::OUTPUT:
797
- out << " OUTPUT" << ' \n ' ; break ;
801
+ out << " OUTPUT" << ' \n ' ;
802
+ break ;
798
803
799
804
case goto_trace_stept::typet::DECL:
800
805
out << " DECL" << ' \n ' ;
@@ -832,29 +837,41 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const
832
837
break ;
833
838
834
839
case goto_trace_stept::typet::DEAD:
835
- out << " DEAD\n " ; break ;
840
+ out << " DEAD\n " ;
841
+ break ;
836
842
case goto_trace_stept::typet::FUNCTION_CALL:
837
- out << " FUNCTION_CALL\n " ; break ;
843
+ out << " FUNCTION_CALL\n " ;
844
+ break ;
838
845
case goto_trace_stept::typet::FUNCTION_RETURN:
839
- out << " FUNCTION_RETURN\n " ; break ;
846
+ out << " FUNCTION_RETURN\n " ;
847
+ break ;
840
848
case goto_trace_stept::typet::CONSTRAINT:
841
- out << " CONSTRAINT\n " ; break ;
849
+ out << " CONSTRAINT\n " ;
850
+ break ;
842
851
case goto_trace_stept::typet::SHARED_READ:
843
- out << " SHARED READ\n " ; break ;
852
+ out << " SHARED READ\n " ;
853
+ break ;
844
854
case goto_trace_stept::typet::SHARED_WRITE:
845
- out << " SHARED WRITE\n " ; break ;
855
+ out << " SHARED WRITE\n " ;
856
+ break ;
846
857
case goto_trace_stept::typet::ATOMIC_BEGIN:
847
- out << " ATOMIC_BEGIN\n " ; break ;
858
+ out << " ATOMIC_BEGIN\n " ;
859
+ break ;
848
860
case goto_trace_stept::typet::ATOMIC_END:
849
- out << " AUTOMIC_END\n " ; break ;
861
+ out << " AUTOMIC_END\n " ;
862
+ break ;
850
863
case goto_trace_stept::typet::SPAWN:
851
- out << " SPAWN\n " ; break ;
864
+ out << " SPAWN\n " ;
865
+ break ;
852
866
case goto_trace_stept::typet::MEMORY_BARRIER:
853
- out << " MEMORY_BARRIER\n " ; break ;
867
+ out << " MEMORY_BARRIER\n " ;
868
+ break ;
854
869
case goto_trace_stept::typet::GOTO:
855
- out << " IF " << format (cond_expr) << " GOTO\n " ; break ;
870
+ out << " IF " << format (cond_expr) << " GOTO\n " ;
871
+ break ;
856
872
857
- default : UNREACHABLE;
873
+ default :
874
+ UNREACHABLE;
858
875
}
859
876
860
877
if (is_assert () || is_assume () || is_assignment () || is_constraint ())
0 commit comments