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