From 33d843320504ea97827ba0b374f76dbb0bf5a0a4 Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Wed, 16 Jan 2013 14:26:19 +0100
Subject: [PATCH] add static checker for constants in contexts
---
de.prob.units/plugin.xml | 12 ++++
.../units/sc/ContextAttributeProcessor.java | 66 +++++++++++++++++++
2 files changed, 78 insertions(+)
create mode 100644 de.prob.units/src/de/prob/units/sc/ContextAttributeProcessor.java
diff --git a/de.prob.units/plugin.xml b/de.prob.units/plugin.xml
index 5e63c917..7ba49ece 100644
--- a/de.prob.units/plugin.xml
+++ b/de.prob.units/plugin.xml
@@ -106,6 +106,9 @@
<scModule
id="de.prob.units.machineAttributeProcessor">
</scModule>
+ <scModule
+ id="de.prob.units.contextAttributeProcessor">
+ </scModule>
</configuration>
</extension>
<extension
@@ -120,5 +123,14 @@
id="org.eventb.core.machineVariableModule">
</prereq>
</processorType>
+ <processorType
+ class="de.prob.units.sc.ContextAttributeProcessor"
+ id="contextAttributeProcessor"
+ name="contextAttributeProcessor"
+ parent="org.eventb.core.contextModule">
+ <prereq
+ id="org.eventb.core.contextConstantModule">
+ </prereq>
+ </processorType>
</extension>
</plugin>
diff --git a/de.prob.units/src/de/prob/units/sc/ContextAttributeProcessor.java b/de.prob.units/src/de/prob/units/sc/ContextAttributeProcessor.java
new file mode 100644
index 00000000..6b420739
--- /dev/null
+++ b/de.prob.units/src/de/prob/units/sc/ContextAttributeProcessor.java
@@ -0,0 +1,66 @@
+package de.prob.units.sc;
+
+import org.eclipse.core.runtime.CoreException;
+import org.eclipse.core.runtime.IProgressMonitor;
+import org.eventb.core.IConstant;
+import org.eventb.core.IContextRoot;
+import org.eventb.core.ISCConstant;
+import org.eventb.core.ISCContextRoot;
+import org.eventb.core.sc.SCCore;
+import org.eventb.core.sc.SCProcessorModule;
+import org.eventb.core.sc.state.ISCStateRepository;
+import org.eventb.core.tool.IModuleType;
+import org.rodinp.core.IInternalElement;
+import org.rodinp.core.IRodinElement;
+import org.rodinp.core.IRodinFile;
+
+import de.prob.units.Activator;
+import de.prob.units.pragmas.UnitPragmaAttribute;
+
+public class ContextAttributeProcessor extends SCProcessorModule {
+ public static final IModuleType<ContextAttributeProcessor> MODULE_TYPE = SCCore
+ .getModuleType(Activator.PLUGIN_ID + ".contextAttributeProcessor"); //$NON-NLS-1$
+
+ @Override
+ public void process(IRodinElement element, IInternalElement target,
+ ISCStateRepository repository, IProgressMonitor monitor)
+ throws CoreException {
+ assert (element instanceof IRodinFile);
+ assert (target instanceof ISCContextRoot);
+
+ // get all variables and copy over the attributes
+ IRodinFile machineFile = (IRodinFile) element;
+ IContextRoot constantRoot = (IContextRoot) machineFile.getRoot();
+
+ ISCContextRoot scContextRoot = (ISCContextRoot) target;
+
+ IConstant[] constants = constantRoot.getConstants();
+
+ if (constants.length == 0)
+ return;
+
+ for (IConstant constant : constants) {
+ ISCConstant scConstant = scContextRoot.getSCConstant(constant
+ .getIdentifierString());
+
+ // might have been filtered out by previous modules
+ if (scConstant != null) {
+ // original might not contain the attribute
+ if (constant.hasAttribute(UnitPragmaAttribute.ATTRIBUTE)) {
+ String attribute = constant
+ .getAttributeValue(UnitPragmaAttribute.ATTRIBUTE);
+
+ scConstant.setAttributeValue(UnitPragmaAttribute.ATTRIBUTE,
+ attribute, monitor);
+ }
+ }
+ }
+
+ }
+
+ @Override
+ public IModuleType<?> getModuleType() {
+ return MODULE_TYPE;
+ }
+
+}
--
GitLab