Skip to content

Commit c0114bc

Browse files
unp1unp1
committed
some fixed for new eclipse and tycho versions
1 parent 997654f commit c0114bc

File tree

7 files changed

+84
-77
lines changed

7 files changed

+84
-77
lines changed

‎JMLEditing/src/features/org.key_project.jmlediting.feature/feature.xml‎

Lines changed: 6 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -126,25 +126,21 @@ Java and all Java-based trademarks are trademarks of Sun Microsystems, Inc. in t
126126
<requires>
127127
<import plugin="org.eclipse.core.runtime"/>
128128
<import plugin="org.eclipse.core.resources"/>
129+
<import plugin="org.eclipse.core.contenttype"/>
129130
<import plugin="org.eclipse.ui"/>
130-
<import plugin="org.eclipse.jface.text"/>
131-
<import plugin="org.eclipse.jdt.core"/>
132-
<import plugin="org.eclipse.jdt.ui"/>
133131
<import plugin="org.eclipse.ui.editors"/>
134132
<import plugin="org.eclipse.ui.ide"/>
133+
<import plugin="org.eclipse.ui.views"/>
134+
<import plugin="org.eclipse.jface"/>
135+
<import plugin="org.eclipse.jface.text"/>
135136
<import plugin="org.eclipse.jdt.core"/>
137+
<import plugin="org.eclipse.jdt.core.manipulation"/>
136138
<import plugin="org.eclipse.jdt.ui"/>
137-
<import plugin="org.eclipse.jface"/>
138139
<import plugin="org.eclipse.ltk.core.refactoring"/>
139-
<import plugin="org.eclipse.ui.views"/>
140-
<import plugin="org.eclipse.emf.common"/>
141140
<import plugin="org.eclipse.e4.ui.model.workbench"/>
142-
<import plugin="org.eclipse.jdt.core"/>
143-
<import plugin="org.eclipse.core.contenttype"/>
141+
<import plugin="org.eclipse.emf.common"/>
144142
<import plugin="org.eclipse.emf.ecore"/>
145143
<import plugin="org.eclipse.emf.edit"/>
146-
<import plugin="org.eclipse.jdt.core.manipulation"/>
147-
<import plugin="org.eclipse.ui"/>
148144
</requires>
149145

150146
<plugin

‎KeYLib/META-INF/MANIFEST.MF‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -256,6 +256,7 @@ Export-Package: antlr,
256256
de.uka.ilkd.key.rule.tacletbuilder,
257257
de.uka.ilkd.key.settings,
258258
de.uka.ilkd.key.smt,
259+
de.uka.ilkd.key.smt.communication,
259260
de.uka.ilkd.key.smt.counterexample,
260261
de.uka.ilkd.key.smt.hierarchy,
261262
de.uka.ilkd.key.smt.lang,

‎KeYLib/de/uka/ilkd/key/smt/newsmt2/DefinedSymbolsHandler.preamble.xml‎

Lines changed: 54 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,19 @@
11
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
22
<!DOCTYPE properties SYSTEM "http://java.sun.com/dtd/properties.dtd">
33
<properties>
4+
<!-- null is the special singleton object in Sort "Null" -->
5+
<entry key="null.dl">
6+
<![CDATA[ \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) ]]>
7+
</entry>
8+
<!-- The function symbols required for Java arithmetics -->
9+
<entry key="javaMulInt.taclets">
10+
translateJavaMulInt
11+
</entry>
12+
13+
<entry key="javaAddInt.taclets">
14+
translateJavaAddInt
15+
</entry>
16+
417
<entry key="seqGetOutside.dl"><![CDATA[
518
\forall int i; \forall Seq s; ( i < 0 | i >= seqLen(s) -> any::seqGet(s, i)<<Trigger>> = seqGetOutside )
619
]]></entry>
@@ -54,6 +67,47 @@
5467
seqLen(seqSub(seq, from, to)<<Trigger>>)
5568
= \if(from < to)\then(to - from)\else(0)
5669
]]></entry>
70+
<!-- The function symbols required for Java arithmetics -->
71+
<entry key="prec.taclets">
72+
precOfInt
73+
</entry>
74+
<entry key="empty.dl">
75+
\forall Object o; \forall Field f; ( elementOf(o,f,empty)&lt;&lt;Trigger&gt;&gt; &lt;-&gt; false )
76+
</entry>
77+
78+
<entry key="union.dl">
79+
\forall Object o; \forall Field f; \forall LocSet l1; \forall LocSet l2;
80+
( elementOf(o, f, union(l1, l2))&lt;&lt;Trigger&gt;&gt; &lt;-&gt; elementOf(o,f,l1) | elementOf(o,f,l2) )
81+
</entry>
82+
83+
<entry key="allLocs.dl">
84+
\forall Object o; \forall Field f; ( elementOf(o,f,allLocs)&lt;&lt;Trigger&gt;&gt; &lt;-&gt; true )
85+
</entry>
86+
87+
<entry key="freshLocs.dl">
88+
\forall Heap h; \forall Object o; \forall Field f;
89+
( elementOf(o,f,freshLocs(h))&lt;&lt;Trigger&gt;&gt; &lt;-&gt;
90+
o != null &amp; !boolean::select(h,o,java.lang.Object::&lt;created&gt;)=TRUE )
91+
</entry>
92+
93+
<entry key="singleton.dl">
94+
\forall Object o; \forall Field f; \forall Object o2; \forall Field f2;
95+
( elementOf(o,f, singleton(o2,f2))&lt;&lt;Trigger&gt;&gt; &lt;-&gt;
96+
o = o2 &amp; f = f2 )
97+
</entry>
98+
99+
<entry key="allFields.dl"><![CDATA[
100+
\forall Object o; \forall Field f; \forall Object o2;
101+
( elementOf(o,f, allFields(o2))<<Trigger>> <->
102+
o = o2 )
103+
]]></entry>
104+
105+
<entry key="arrayRange.dl"><![CDATA[
106+
\forall Object o; \forall Object o2; \forall Field f; \forall int lo; \forall int hi;
107+
(elementOf(o,f, arrayRange(o2, lo, hi))<<Trigger>> <->
108+
o = o2 & \exists int iv; (f = arr(iv) & lo <= iv & iv <= hi))
109+
]]></entry>
110+
57111
<entry key="store.dl"><![CDATA[
58112
\forall Heap h; \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; \forall any v;
59113
any::select(store(h,o,f,v), o2, f2)<<Trigger>> =
@@ -98,58 +152,4 @@
98152
]]></entry>
99153

100154
<!-- to be done: all objects inside location sets in fields in wellFormed heaps are created or null -->
101-
<!-- null is the special singleton object in Sort "Null" -->
102-
<entry key="null.dl">
103-
<![CDATA[ \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) ]]>
104-
</entry>
105-
<!-- The function symbols required for Java arithmetics -->
106-
<entry key="javaMulInt.taclets">
107-
translateJavaMulInt
108-
</entry>
109-
110-
<entry key="javaAddInt.taclets">
111-
translateJavaAddInt
112-
</entry>
113-
114-
<!-- The function symbols required for Java arithmetics -->
115-
<entry key="prec.taclets">
116-
precOfInt
117-
</entry>
118-
<entry key="empty.dl">
119-
\forall Object o; \forall Field f; ( elementOf(o,f,empty)&lt;&lt;Trigger&gt;&gt; &lt;-&gt; false )
120-
</entry>
121-
122-
<entry key="union.dl">
123-
\forall Object o; \forall Field f; \forall LocSet l1; \forall LocSet l2;
124-
( elementOf(o, f, union(l1, l2))&lt;&lt;Trigger&gt;&gt; &lt;-&gt; elementOf(o,f,l1) | elementOf(o,f,l2) )
125-
</entry>
126-
127-
<entry key="allLocs.dl">
128-
\forall Object o; \forall Field f; ( elementOf(o,f,allLocs)&lt;&lt;Trigger&gt;&gt; &lt;-&gt; true )
129-
</entry>
130-
131-
<entry key="freshLocs.dl">
132-
\forall Heap h; \forall Object o; \forall Field f;
133-
( elementOf(o,f,freshLocs(h))&lt;&lt;Trigger&gt;&gt; &lt;-&gt;
134-
o != null &amp; !boolean::select(h,o,java.lang.Object::&lt;created&gt;)=TRUE )
135-
</entry>
136-
137-
<entry key="singleton.dl">
138-
\forall Object o; \forall Field f; \forall Object o2; \forall Field f2;
139-
( elementOf(o,f, singleton(o2,f2))&lt;&lt;Trigger&gt;&gt; &lt;-&gt;
140-
o = o2 &amp; f = f2 )
141-
</entry>
142-
143-
<entry key="allFields.dl"><![CDATA[
144-
\forall Object o; \forall Field f; \forall Object o2;
145-
( elementOf(o,f, allFields(o2))<<Trigger>> <->
146-
o = o2 )
147-
]]></entry>
148-
149-
<entry key="arrayRange.dl"><![CDATA[
150-
\forall Object o; \forall Object o2; \forall Field f; \forall int lo; \forall int hi;
151-
(elementOf(o,f, arrayRange(o2, lo, hi))<<Trigger>> <->
152-
o = o2 & \exists int iv; (f = arr(iv) & lo <= iv & iv <= hi))
153-
]]></entry>
154-
155155
</properties>

‎KeYLib/de/uka/ilkd/key/util/branch‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
heads/KeY-2.10.0
1+
KeY-2.10.0

‎KeYLib/examples.zip‎

-275 KB
Binary file not shown.

‎VisualDbC/src/features/de.hentschel.visualdbc.feature/feature.xml‎

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,6 @@ Java and all Java-based trademarks are trademarks of Sun Microsystems, Inc. in t
132132

133133
<requires>
134134
<import plugin="org.eclipse.core.runtime"/>
135-
<import plugin="org.eclipse.ui"/>
136135
<import plugin="org.eclipse.core.resources"/>
137136
<import plugin="org.key_project.util"/>
138137
<import plugin="org.key_project.core"/>
@@ -142,15 +141,22 @@ Java and all Java-based trademarks are trademarks of Sun Microsystems, Inc. in t
142141
<import plugin="org.eclipse.emf.ecore"/>
143142
<import plugin="org.eclipse.core.expressions"/>
144143
<import plugin="org.eclipse.jface"/>
144+
<import plugin="org.eclipse.ui"/>
145145
<import plugin="org.eclipse.ui.ide"/>
146146
<import plugin="org.eclipse.ui.views"/>
147147
<import plugin="org.eclipse.ui.navigator"/>
148148
<import plugin="org.eclipse.ui.navigator.resources"/>
149+
<import plugin="org.eclipse.ui.intro"/>
150+
<import plugin="org.eclipse.emf"/>
151+
<import plugin="org.eclipse.emf.common.ui"/>
149152
<import plugin="org.eclipse.emf.ecore.xmi"/>
153+
<import plugin="org.eclipse.emf.edit"/>
150154
<import plugin="org.eclipse.emf.edit.ui"/>
155+
<import plugin="org.eclipse.emf.transaction"/>
151156
<import plugin="org.eclipse.gmf.runtime.emf.core"/>
152157
<import plugin="org.eclipse.gmf.runtime.emf.commands.core"/>
153158
<import plugin="org.eclipse.gmf.runtime.emf.ui.properties"/>
159+
<import plugin="org.eclipse.gmf.runtime.diagram.core"/>
154160
<import plugin="org.eclipse.gmf.runtime.diagram.ui"/>
155161
<import plugin="org.eclipse.gmf.runtime.diagram.ui.properties"/>
156162
<import plugin="org.eclipse.gmf.runtime.diagram.ui.providers"/>
@@ -160,18 +166,11 @@ Java and all Java-based trademarks are trademarks of Sun Microsystems, Inc. in t
160166
<import plugin="org.eclipse.gmf.runtime.diagram.ui.resources.editor.ide"/>
161167
<import plugin="org.eclipse.draw2d"/>
162168
<import plugin="org.eclipse.gmf.runtime.draw2d.ui"/>
169+
<import plugin="org.eclipse.gmf.runtime.notation"/>
163170
<import plugin="org.eclipse.ocl.ecore"/>
164171
<import plugin="org.eclipse.gef"/>
165-
<import plugin="org.eclipse.emf.edit"/>
166-
<import plugin="org.eclipse.emf.transaction"/>
167-
<import plugin="org.eclipse.gmf.runtime.notation"/>
168-
<import plugin="org.eclipse.gmf.runtime.diagram.core"/>
169-
<import plugin="org.eclipse.ui.navigator.resources"/>
170-
<import plugin="org.eclipse.ui.intro"/>
171172
<import plugin="org.eclipse.jdt.core"/>
172173
<import plugin="org.eclipse.jdt.ui"/>
173-
<import plugin="org.eclipse.emf.common.ui"/>
174-
<import plugin="org.eclipse.emf"/>
175174
<import plugin="org.key_project.key4eclipse.common.ui"/>
176175
<import plugin="org.eclipse.help"/>
177176
<import plugin="org.key_project.core.symbolic_execution"/>

‎pom.xml‎

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@
1515
<version>0.1.0-SNAPSHOT</version>
1616

1717
<properties>
18-
<tools.mdsd.dependencies.eclipse-version>2021-12</tools.mdsd.dependencies.eclipse-version>
19-
<tycho.version>2.2.0</tycho.version>
18+
<tools.mdsd.dependencies.eclipse-version>2022-03</tools.mdsd.dependencies.eclipse-version>
19+
<tycho.version>2.7.3</tycho.version>
2020
<tycho-javadoc.version>2.2.0</tycho-javadoc.version>
2121
<javadoc.args>
2222
-tag "generated:a:Generated class or method."
@@ -29,7 +29,7 @@
2929
-tag 'nooverride:a:Restriction:'
3030
-tag 'category:a:Category:'
3131
-link ${java.api.doc}
32-
-link http://help.eclipse.org/2020-12/topic/org.eclipse.platform.doc.isv/reference/api
32+
-link http://help.eclipse.org/2022-03/topic/org.eclipse.platform.doc.isv/reference/api
3333
-link https://download.eclipse.org/modeling/emf/emf/javadoc/2.11/
3434
-link https://download.eclipse.org/modeling/emft/mwe/javadoc/2.9/
3535
</javadoc.args>
@@ -117,6 +117,17 @@
117117

118118
<build>
119119
<plugins>
120+
<plugin>
121+
<groupId>org.apache.maven.plugins</groupId>
122+
<artifactId>maven-site-plugin</artifactId>
123+
<version>3.12.0</version>
124+
</plugin>
125+
<plugin>
126+
<groupId>org.apache.maven.plugins</groupId>
127+
<artifactId>maven-project-info-reports-plugin</artifactId>
128+
<version>3.0.0</version>
129+
</plugin>
130+
120131
<plugin>
121132
<groupId>org.eclipse.tycho</groupId>
122133
<artifactId>tycho-compiler-plugin</artifactId>

0 commit comments

Comments
 (0)