Skip to content

Commit

Permalink
Merge pull request #2543 from mbeddr/refactoring/cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@alexanderpann
alexanderpann authored Oct 6, 2024
2 parents c196e68 + 9e3c970 commit f213038
Show file tree
Hide file tree
Showing 170 changed files with 153 additions and 33,733 deletions.
5 changes: 5 additions & 0 deletions code/applications/HeartBleed/.mps/migration.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,11 @@
<entry key="jetbrains.mps.ide.mpsmigration.v35.RemoveHistoryFiles" value="executed" />
<entry key="jetbrains.mps.ide.mpsmigration.v35.SetGenRequiredToEmptyAspects" value="executed" />
<entry key="jetbrains.mps.ide.mpsmigration.v_2019_3.DefaultFacetExplicitPersistence" value="executed" />
<entry key="jetbrains.mps.ide.mpsmigration.v_2021_2.SplitMPSCoreStub" value="executed" />
<entry key="jetbrains.mps.ide.mpsmigration.v_2021_3.ExtractMPSBootStubs" value="executed" />
<entry key="jetbrains.mps.ide.mpsmigration.v_2022_3.ExplicitJavaFacetSettings" value="executed" />
<entry key="jetbrains.mps.ide.mpsmigration.v_2022_3.SplitMPSCoreStub2" value="executed" />
<entry key="jetbrains.mps.v8_elimination" value="executed" />
<entry key="project.migrated.version" value="223" />
</component>
</project>
8 changes: 0 additions & 8 deletions code/applications/HeartBleed/solutions/NewSolution.msd
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@
<language slang="l:efda956e-491e-4f00-ba14-36af2f213ecf:com.mbeddr.core.udt" version="5" />
<language slang="l:06d68b77-b699-4918-83b8-857e63787800:com.mbeddr.core.unittest" version="4" />
<language slang="l:2693fc71-9b0e-4b05-ab13-f57227d675f2:com.mbeddr.core.util" version="0" />
<language slang="l:b574d547-b77e-4fed-9f60-c349c4410765:com.mbeddr.ext.math" version="0" />
<language slang="l:63e0e566-5131-447e-90e3-12ea330e1a00:com.mbeddr.mpsutil.blutil" version="3" />
<language slang="l:d3a0fd26-445a-466c-900e-10444ddfed52:com.mbeddr.mpsutil.filepicker" version="0" />
<language slang="l:1c897ba5-9d43-4035-ac7f-0306495743ac:com.mbeddr.mpsutil.interpreter.test" version="0" />
Expand All @@ -53,14 +52,7 @@
<language slang="l:7a5dda62-9140-4668-ab76-d5ed1746f2b2:jetbrains.mps.lang.typesystem" version="5" />
</languageVersions>
<dependencyVersions>
<module reference="3f233e7f-b8a6-46d2-a57f-795d56775243(Annotations)" version="0" />
<module reference="1d9e6da7-9a83-410c-b177-32cc0c2e3c03(HeartBleedImpl)" version="0" />
<module reference="6354ebe7-c22a-4a0f-ac54-50b52ab9b065(JDK)" version="0" />
<module reference="6ed54515-acc8-4d1e-a16c-9fd6cfe951ea(MPS.Core)" version="0" />
<module reference="1ed103c3-3aa6-49b7-9c21-6765ee11f224(MPS.Editor)" version="0" />
<module reference="498d89d2-c2e9-11e2-ad49-6cf049e62fe5(MPS.IDEA)" version="0" />
<module reference="8865b7a8-5271-43d3-884c-6fd1d9cfdd34(MPS.OpenAPI)" version="0" />
<module reference="742f6602-5a2f-4313-aa6e-ae1cd4ffdc61(MPS.Platform)" version="0" />
<module reference="fbe54499-edb8-4097-b473-699993bd8a01(com.mbeddr.analyses.cbmc.core.pluginSolution)" version="0" />
<module reference="9506d0a9-4e49-4605-b51a-d3aeb0070ba3(com.mbeddr.analyses.cbmc.core.rt)" version="0" />
<module reference="397da8bd-bcff-4d80-87cb-c4eaba8e2cb2(com.mbeddr.analyses.cbmc.pluginSolution)" version="0" />
Expand Down
107 changes: 0 additions & 107 deletions code/applications/HeartBleed/solutions/models/HearBleedImpl/Model1.mps
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@
<languages>
<use id="92d2ea16-5a42-4fdf-a676-c7604efe3504" name="de.slisson.mps.richtext" version="0" />
<devkit ref="d2a9c55c-6bdc-4cc2-97e1-4ba7552f5584(com.mbeddr.core)" />
<devkit ref="0ca77142-1eea-4b14-b369-69bdaa1c44fb(com.mbeddr.analyses.core)" />
</languages>
<imports />
<registry>
Expand Down Expand Up @@ -81,36 +80,6 @@
<child id="1452920870317474611" name="sizeExpr" index="1YbSNA" />
</concept>
</language>
<language id="0a02a8f9-14d0-4970-9bd2-ca35a097c80d" name="com.mbeddr.analyses.cbmc.core">
<concept id="4053481679317021366" name="com.mbeddr.analyses.cbmc.core.structure.RobustnessCBMCAnalysis" flags="ng" index="1nvAUE">
<property id="4053481679317021372" name="check_nan" index="1nvAUw" />
<property id="4053481679317021368" name="check_pointer" index="1nvAU$" />
<property id="4053481679317021369" name="check_array_bounds" index="1nvAU_" />
<property id="4053481679317021370" name="check_signed_overflow" index="1nvAUA" />
<property id="4053481679317021371" name="check_unsigned_overflow" index="1nvAUB" />
<property id="4053481679317021367" name="check_div_by_zero" index="1nvAUF" />
</concept>
</language>
<language id="42270baf-e92c-4c32-b263-d617b3fce239" name="com.mbeddr.analyses.cbmc">
<concept id="8985851583396455245" name="com.mbeddr.analyses.cbmc.structure.NondetVarAssignment" flags="ng" index="2c3wGE">
<property id="2613206384568936346" name="constraintsEnabled" index="2xg5V6" />
<child id="8985851583396455257" name="varRef" index="2c3wGY" />
</concept>
<concept id="8985851583396455243" name="com.mbeddr.analyses.cbmc.structure.HarnessModule" flags="ng" index="2c3wGG" />
<concept id="8327535879610131181" name="com.mbeddr.analyses.cbmc.structure.ICbmcSettings" flags="ng" index="2lUzGJ">
<property id="8327535879610783176" name="timeoutInSeconds" index="2l50Ka" />
<property id="8327535879610783188" name="timeoutForSingleAnalysis" index="2l50Km" />
<property id="8327535879610783060" name="sliceFormula" index="2l50Mm" />
<property id="8327535879610145579" name="analysisDepth" index="2lUGbD" />
<property id="8327535879610145347" name="hasUnwindingDepth" index="2lUGe1" />
<property id="8327535879610145405" name="unwindingAssertions" index="2lUGeZ" />
<property id="8327535879610142482" name="unwindingDepth" index="2lUHrg" />
</concept>
<concept id="2135612507694884868" name="com.mbeddr.analyses.cbmc.structure.CBMCAnalysisConfigurationContainer" flags="ng" index="3uEX16" />
<concept id="6472990431939799907" name="com.mbeddr.analyses.cbmc.structure.CProverBasedAnalysis" flags="ng" index="3V$Cnz">
<reference id="6472990431939799908" name="entryPoint" index="3V$Cn$" />
</concept>
</language>
<language id="2693fc71-9b0e-4b05-ab13-f57227d675f2" name="com.mbeddr.core.util">
<concept id="4459718605982051949" name="com.mbeddr.core.util.structure.ReportingConfiguration" flags="ng" index="2Q9Fgs">
<child id="4459718605982051999" name="strategy" index="2Q9FjI" />
Expand Down Expand Up @@ -180,12 +149,6 @@
<reference id="2093108837558505659" name="arg" index="3ZUYvu" />
</concept>
</language>
<language id="5d09074f-babf-4f2b-b78b-e9929af0f3be" name="com.mbeddr.analyses.base">
<concept id="6472990431939580591" name="com.mbeddr.analyses.base.structure.AnalysisConfiguration" flags="ng" index="3V_BKJ">
<child id="6472990431939692464" name="analyses" index="3V$2$K" />
<child id="559958203687603517" name="imports" index="3W6d8T" />
</concept>
</language>
<language id="ceab5195-25ea-4f22-9b92-103b95ca8c0c" name="jetbrains.mps.lang.core">
<concept id="1133920641626" name="jetbrains.mps.lang.core.structure.BaseConcept" flags="ng" index="2VYdi">
<child id="5169995583184591170" name="smodelAttribute" index="lGtFl" />
Expand Down Expand Up @@ -401,19 +364,6 @@
</node>
</node>
</node>
<node concept="2c3wGG" id="1W6K2BBDSHl" role="3XIRFZ">
<node concept="2c3wGE" id="1W6K2BBDXKI" role="3XIRFZ">
<property role="2xg5V6" value="false" />
<node concept="2qmXGp" id="1W6K2BBDYhV" role="2c3wGY">
<node concept="1E4Tgc" id="1W6K2BBDYAT" role="1ESnxz">
<ref role="1E4Tge" node="4yOgC5DNkzS" resolve="payload_length" />
</node>
<node concept="3ZVu4v" id="1W6K2BBDYhS" role="1_9fRO">
<ref role="3ZVs_2" node="1W6K2BBAm0B" resolve="m" />
</node>
</node>
</node>
</node>
<node concept="2BFjQ_" id="1W6K2BBArRh" role="3XIRFZ">
<node concept="3ZVu4v" id="1W6K2BBAsj3" role="2BFjQA">
<ref role="3ZVs_2" node="1W6K2BBAm0B" resolve="m" />
Expand Down Expand Up @@ -1366,62 +1316,5 @@
</node>
</node>
</node>
<node concept="3uEX16" id="2N9rEs47IR">
<property role="2l50Ka" value="none" />
<property role="2l50Km" value="none" />
<property role="2lUGeZ" value="true" />
<property role="2lUHrg" value="25" />
<property role="2lUGe1" value="true" />
<property role="2lUGbD" value="none" />
<property role="TrG5h" value="Analyses" />
<node concept="1nvAUE" id="2N9rEs47IS" role="3V$2$K">
<property role="2lUGeZ" value="false" />
<property role="2lUHrg" value="25" />
<property role="2lUGbD" value="none" />
<property role="2l50Ka" value="none" />
<property role="2l50Km" value="none" />
<property role="2l50Mm" value="false" />
<property role="1nvAU_" value="true" />
<property role="1nvAUF" value="true" />
<property role="1nvAUw" value="true" />
<property role="1nvAU$" value="true" />
<property role="1nvAUA" value="true" />
<property role="1nvAUB" value="true" />
<ref role="3V$Cn$" node="1W6K2BB_NAm" resolve="verification" />
</node>
<node concept="1nvAUE" id="2N9rEs47IT" role="3V$2$K">
<property role="2lUGeZ" value="false" />
<property role="2lUHrg" value="25" />
<property role="2lUGbD" value="none" />
<property role="2l50Ka" value="none" />
<property role="2l50Km" value="none" />
<property role="2l50Mm" value="false" />
<property role="1nvAU_" value="true" />
<property role="1nvAUF" value="true" />
<property role="1nvAUw" value="true" />
<property role="1nvAU$" value="true" />
<property role="1nvAUA" value="true" />
<property role="1nvAUB" value="true" />
<ref role="3V$Cn$" node="1nKwQCIU2W7" resolve="verificationFixed" />
</node>
<node concept="1nvAUE" id="2N9rEs47IU" role="3V$2$K">
<property role="2lUGeZ" value="false" />
<property role="2lUHrg" value="25" />
<property role="2lUGbD" value="none" />
<property role="2l50Ka" value="none" />
<property role="2l50Km" value="none" />
<property role="2l50Mm" value="false" />
<property role="1nvAUw" value="true" />
<property role="1nvAU$" value="true" />
<property role="1nvAUA" value="true" />
<property role="1nvAUB" value="true" />
<property role="1nvAU_" value="true" />
<property role="1nvAUF" value="true" />
<ref role="3V$Cn$" node="21ftQP2zJmX" resolve="testRobustness" />
</node>
<node concept="3GEVxB" id="2N9rEs47J4" role="3W6d8T">
<ref role="3GEb4d" node="4yOgC5DNb4L" resolve="HeartBleed" />
</node>
</node>
</model>

5 changes: 5 additions & 0 deletions code/applications/IntegratedCExample/.mps/migration.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,10 +14,15 @@
<entry key="jetbrains.mps.ide.mpsmigration.v35.RemoveHistoryFiles" value="executed" />
<entry key="jetbrains.mps.ide.mpsmigration.v35.SetGenRequiredToEmptyAspects" value="executed" />
<entry key="jetbrains.mps.ide.mpsmigration.v_2019_3.DefaultFacetExplicitPersistence" value="executed" />
<entry key="jetbrains.mps.ide.mpsmigration.v_2021_2.SplitMPSCoreStub" value="executed" />
<entry key="jetbrains.mps.ide.mpsmigration.v_2021_3.ExtractMPSBootStubs" value="executed" />
<entry key="jetbrains.mps.ide.mpsmigration.v_2022_3.ExplicitJavaFacetSettings" value="executed" />
<entry key="jetbrains.mps.ide.mpsmigration.v_2022_3.SplitMPSCoreStub2" value="executed" />
<entry key="jetbrains.mps.name2id_gen_perroot" value="executed" />
<entry key="jetbrains.mps.obsoletePropsCleanup" value="executed" />
<entry key="jetbrains.mps.projectJavaVersionMigration" value="executed" />
<entry key="jetbrains.mps.resaveModules" value="executed" />
<entry key="jetbrains.mps.v8_elimination" value="executed" />
<entry key="project.migrated.version" value="223" />
</component>
</project>
8 changes: 0 additions & 8 deletions ...plications/IntegratedCExample/languages/DomainSpecificLanguage/DomainSpecificLanguage.mpl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -95,11 +95,8 @@
<module reference="fd392034-7849-419d-9071-12563d152375(jetbrains.mps.baseLanguage.closures)" version="0" />
<module reference="83888646-71ce-4f1c-9c53-c54016f6ad4f(jetbrains.mps.baseLanguage.collections)" version="0" />
<module reference="e39e4a59-8cb6-498e-860e-8fa8361c0d90(jetbrains.mps.baseLanguage.scopes)" version="0" />
<module reference="fdaaf35f-8ee3-4c37-b09d-9efaeaaa7a41(jetbrains.mps.core.tool.environment)" version="0" />
<module reference="cc7da2f6-419f-4133-a811-31fcd3295a85(jetbrains.mps.debugger.api.api)" version="0" />
<module reference="23865718-e2ed-41b5-a132-0da1d04e266d(jetbrains.mps.ide.httpsupport.manager)" version="0" />
<module reference="ae6d8005-36be-4cb6-945b-8c8cfc033c51(jetbrains.mps.ide.httpsupport.runtime)" version="0" />
<module reference="8d29d73f-ed99-4652-ae0a-083cdfe53c34(jetbrains.mps.ide.platform)" version="0" />
<module reference="2d3c70e9-aab2-4870-8d8d-6036800e4103(jetbrains.mps.kernel)" version="0" />
<module reference="d936855b-48da-4812-a8a0-2bfddd633ac5(jetbrains.mps.lang.behavior.api)" version="0" />
<module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
Expand All @@ -110,7 +107,6 @@
<module reference="9ded098b-ad6a-4657-bfd9-48636cfe8bc3(jetbrains.mps.lang.traceable)" version="0" />
<module reference="7a5dda62-9140-4668-ab76-d5ed1746f2b2(jetbrains.mps.lang.typesystem)" version="0" />
<module reference="5187f5c9-b8a8-4309-90b3-14f9919bd2d8(jetbrains.mps.refactoring)" version="0" />
<module reference="8fe4c62a-2020-4ff4-8eda-f322a55bdc9f(jetbrains.mps.refactoring.runtime)" version="0" />
</dependencyVersions>
<mapping-priorities />
</generator>
Expand Down Expand Up @@ -192,11 +188,8 @@
<module reference="fd392034-7849-419d-9071-12563d152375(jetbrains.mps.baseLanguage.closures)" version="0" />
<module reference="83888646-71ce-4f1c-9c53-c54016f6ad4f(jetbrains.mps.baseLanguage.collections)" version="0" />
<module reference="e39e4a59-8cb6-498e-860e-8fa8361c0d90(jetbrains.mps.baseLanguage.scopes)" version="0" />
<module reference="fdaaf35f-8ee3-4c37-b09d-9efaeaaa7a41(jetbrains.mps.core.tool.environment)" version="0" />
<module reference="cc7da2f6-419f-4133-a811-31fcd3295a85(jetbrains.mps.debugger.api.api)" version="0" />
<module reference="23865718-e2ed-41b5-a132-0da1d04e266d(jetbrains.mps.ide.httpsupport.manager)" version="0" />
<module reference="ae6d8005-36be-4cb6-945b-8c8cfc033c51(jetbrains.mps.ide.httpsupport.runtime)" version="0" />
<module reference="8d29d73f-ed99-4652-ae0a-083cdfe53c34(jetbrains.mps.ide.platform)" version="0" />
<module reference="2d3c70e9-aab2-4870-8d8d-6036800e4103(jetbrains.mps.kernel)" version="0" />
<module reference="d936855b-48da-4812-a8a0-2bfddd633ac5(jetbrains.mps.lang.behavior.api)" version="0" />
<module reference="ceab5195-25ea-4f22-9b92-103b95ca8c0c(jetbrains.mps.lang.core)" version="0" />
Expand All @@ -208,7 +201,6 @@
<module reference="9ded098b-ad6a-4657-bfd9-48636cfe8bc3(jetbrains.mps.lang.traceable)" version="0" />
<module reference="7a5dda62-9140-4668-ab76-d5ed1746f2b2(jetbrains.mps.lang.typesystem)" version="0" />
<module reference="5187f5c9-b8a8-4309-90b3-14f9919bd2d8(jetbrains.mps.refactoring)" version="0" />
<module reference="8fe4c62a-2020-4ff4-8eda-f322a55bdc9f(jetbrains.mps.refactoring.runtime)" version="0" />
</dependencyVersions>
<extendedLanguages>
<extendedLanguage>2374bc90-7e37-41f1-a9c4-c2e35194c36a(com.mbeddr.doc)</extendedLanguage>
Expand Down
6 changes: 0 additions & 6 deletions code/applications/IntegratedCExample/solutions/EmbeddedProgram/models/main_sm.mps
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,18 +8,13 @@
<use id="3bf5377a-e904-4ded-9754-5a516023bfaa" name="com.mbeddr.core.pointers" version="0" />
<use id="92d2ea16-5a42-4fdf-a676-c7604efe3504" name="de.slisson.mps.richtext" version="0" />
<use id="61c69711-ed61-4850-81d9-7714ff227fb0" name="com.mbeddr.core.expressions" version="5" />
<use id="b574d547-b77e-4fed-9f60-c349c4410765" name="com.mbeddr.ext.math" version="0" />
<use id="d4280a54-f6df-4383-aa41-d1b2bffa7eb1" name="com.mbeddr.core.base" version="6" />
<use id="6d11763d-483d-4b2b-8efc-09336c1b0001" name="com.mbeddr.core.modules" version="5" />
<use id="daa1849d-6955-4fef-afe3-8aea1f61e6fa" name="com.mbeddr.analyses.cbmc.statemachines" version="0" />
<use id="a9d69647-0840-491e-bf39-2eb0805d2011" name="com.mbeddr.core.statements" version="2" />
<use id="efda956e-491e-4f00-ba14-36af2f213ecf" name="com.mbeddr.core.udt" version="5" />
</languages>
<imports />
<registry>
<language id="daa1849d-6955-4fef-afe3-8aea1f61e6fa" name="com.mbeddr.analyses.cbmc.statemachines">
<concept id="6085839724193282957" name="com.mbeddr.analyses.cbmc.statemachines.structure.StatemachineCheckAttribute" flags="ng" index="1WXklL" />
</language>
<language id="a9d69647-0840-491e-bf39-2eb0805d2011" name="com.mbeddr.core.statements">
<concept id="8441331188640771826" name="com.mbeddr.core.statements.structure.WhileStatement" flags="ng" index="27v$Wf">
<child id="8441331188640771828" name="body" index="27v$W9" />
Expand Down Expand Up @@ -1500,7 +1495,6 @@
</node>
</node>
</node>
<node concept="1WXklL" id="16prvoWGuN9" role="lGtFl" />
</node>
<node concept="2NXPZ9" id="6lKxXE1FIQF" role="N3F5h">
<property role="TrG5h" value="empty_1409950927437_19" />
Expand Down
6 changes: 0 additions & 6 deletions code/applications/IntegratedCExample/solutions/EmbeddedProgram/models/main_sm_controller.mps
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,18 +9,13 @@
<use id="92d2ea16-5a42-4fdf-a676-c7604efe3504" name="de.slisson.mps.richtext" version="0" />
<use id="442192fc-0a8e-4f77-b358-f47f229809d1" name="DomainSpecificLanguage" version="0" />
<use id="61c69711-ed61-4850-81d9-7714ff227fb0" name="com.mbeddr.core.expressions" version="5" />
<use id="b574d547-b77e-4fed-9f60-c349c4410765" name="com.mbeddr.ext.math" version="0" />
<use id="d4280a54-f6df-4383-aa41-d1b2bffa7eb1" name="com.mbeddr.core.base" version="6" />
<use id="6d11763d-483d-4b2b-8efc-09336c1b0001" name="com.mbeddr.core.modules" version="5" />
<use id="daa1849d-6955-4fef-afe3-8aea1f61e6fa" name="com.mbeddr.analyses.cbmc.statemachines" version="0" />
<use id="a9d69647-0840-491e-bf39-2eb0805d2011" name="com.mbeddr.core.statements" version="2" />
<use id="efda956e-491e-4f00-ba14-36af2f213ecf" name="com.mbeddr.core.udt" version="5" />
</languages>
<imports />
<registry>
<language id="daa1849d-6955-4fef-afe3-8aea1f61e6fa" name="com.mbeddr.analyses.cbmc.statemachines">
<concept id="6085839724193282957" name="com.mbeddr.analyses.cbmc.statemachines.structure.StatemachineCheckAttribute" flags="ng" index="1WXklL" />
</language>
<language id="a9d69647-0840-491e-bf39-2eb0805d2011" name="com.mbeddr.core.statements">
<concept id="8441331188640771826" name="com.mbeddr.core.statements.structure.WhileStatement" flags="ng" index="27v$Wf">
<child id="8441331188640771828" name="body" index="27v$W9" />
Expand Down Expand Up @@ -1518,7 +1513,6 @@
<node concept="2xGTIE" id="Ll6J3crBMx" role="S7lxW" />
</node>
</node>
<node concept="1WXklL" id="3Mo_eVXtBu6" role="lGtFl" />
</node>
<node concept="2NXPZ9" id="7iLD7IPXk5s" role="N3F5h">
<property role="TrG5h" value="empty_1409950927437_19" />
Expand Down
Loading

0 comments on commit f213038

Please sign in to comment.