File tree Expand file tree Collapse file tree 3 files changed +26
-24
lines changed
main/java/de/uka/ilkd/key
test/java/de/uka/ilkd/key/parser Expand file tree Collapse file tree 3 files changed +26
-24
lines changed Original file line number Diff line number Diff line change 1818import de .uka .ilkd .key .nparser .ParsingFacade ;
1919import de .uka .ilkd .key .rule .RuleSet ;
2020
21- import de .uka .ilkd .key .util .parsing .BuildingIssue ;
2221import org .key_project .util .collection .DefaultImmutableSet ;
2322import org .key_project .util .collection .ImmutableSet ;
2423
2524import org .antlr .v4 .runtime .Token ;
2625import org .slf4j .Logger ;
2726import org .slf4j .LoggerFactory ;
28- import recoder .util .Debug ;
2927
3028/**
3129 * This visitor evaluates all basic (level 0) declarations. This includes:
@@ -159,11 +157,12 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) {
159157 sorts ().add (s );
160158 createdSorts .add (s );
161159 } else {
162- // weigl: agreement on KaKeY meeting: this should be ignored until we finally have local namespaces
160+ // weigl: agreement on KaKeY meeting: this should be ignored until we finally have
161+ // local namespaces
163162 // for generic sorts
164- //addWarning(ctx, "Sort declaration is ignored, due to collision.");
163+ // addWarning(ctx, "Sort declaration is ignored, due to collision.");
165164 LOGGER .info ("Sort declaration is ignored, due to collision in {}" ,
166- BuilderHelpers .getPosition (ctx ));
165+ BuilderHelpers .getPosition (ctx ));
167166 }
168167 }
169168 return createdSorts ;
Original file line number Diff line number Diff line change 55
66import java .net .URI ;
77import java .net .URISyntaxException ;
8+
89import de .uka .ilkd .key .java .Position ;
910import de .uka .ilkd .key .parser .Location ;
1011import de .uka .ilkd .key .speclang .PositionedString ;
Original file line number Diff line number Diff line change @@ -46,25 +46,27 @@ protected Services getServices() {
4646
4747 @ BeforeEach
4848 public void setUp () throws IOException {
49- parseDecls ("""
50- \\ sorts { boolean; elem; list; int; int_sort; numbers; }
51- \\ functions {
52- elem head(list);
53- list tail(list);
54- list nil;
55- list cons(elem,list);
56- int aa ;
57- int bb ;
58- int cc ;
59- int dd ;
60- int ee ;
61- }
62- \\ predicates {
63- isempty(list);
64- }
65- \\ programVariables {int globalIntPV;}"""
66-
67- );
49+ if (lookup_sort ("elem" ) == null ) {// check whether declaration have already been parsed
50+ parseDecls ("""
51+ \\ sorts { boolean; elem; list; int; int_sort; numbers; }
52+ \\ functions {
53+ elem head(list);
54+ list tail(list);
55+ list nil;
56+ list cons(elem,list);
57+ int aa ;
58+ int bb ;
59+ int cc ;
60+ int dd ;
61+ int ee ;
62+ }
63+ \\ predicates {
64+ isempty(list);
65+ }
66+ \\ programVariables {int globalIntPV;}"""
67+
68+ );
69+ }
6870
6971 elem = lookup_sort ("elem" );
7072 list = lookup_sort ("list" );
You can’t perform that action at this time.
0 commit comments