update cl args

.gitignore

@@ -1,5 +1,6 @@
 **/.IR
 **/.aadlbin-gen/
+**/.bloop/
 **/.settings/
 **/instances
 **/c/nix

isolette/aadl/bin/run-hamr.cmd

@@ -60,7 +60,7 @@ val platform: String =
 val codegenArgs = ISZ("hamr", "codegen",
   "--platform", platform,
   "--package-name", packageName,
-  "--output-dir", (aadlDir.up / "hamr" / "slang").string,
+  "--output-dir", (aadlDir.up / "hamr").string,
   "--output-c-dir", (aadlDir.up / "hamr" / "c").string,
   "--run-transpiler",
   "--bit-width", "32",
@@ -69,7 +69,7 @@ val codegenArgs = ISZ("hamr", "codegen",
   "--exclude-component-impl",
   "--verbose",
   //"--no-proyek-ive",
-  "--aadl-root-dir", aadlDir.string,
+  "--workspace-root-dir", aadlDir.string,
   (aadlDir / ".system").string)
 
 val results = Os.proc(osireum ++ codegenArgs).console.run()

isolette/hamr/c/bin/compile.cmd

@@ -1,17 +1,17 @@
 ::/*#! 2> /dev/null                                   #
 @ 2>/dev/null # 2>nul & echo off & goto BOF           #
-if [ -z ${SIREUM_HOME} ]; then                       #
+if [ -z "${SIREUM_HOME}" ]; then                     #
   echo "Please set SIREUM_HOME env var"               #
   exit -1                                             #
 fi                                                    #
-exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" #
+exec "${SIREUM_HOME}/bin/sireum" slang run "$0" "$@" #
 :BOF
 setlocal
 if not defined SIREUM_HOME (
   echo Please set SIREUM_HOME env var
   exit /B -1
 )
-%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+"%SIREUM_HOME%\bin\sireum.bat" slang run %0 %*
 exit /B %errorlevel%
 ::!#*/
 // #Sireum

isolette/hamr/slang/bin/project.cmd

@@ -1,17 +1,17 @@
 ::/*#! 2> /dev/null                                   #
 @ 2>/dev/null # 2>nul & echo off & goto BOF           #
-if [ -z ${SIREUM_HOME} ]; then                        #
+if [ -z "${SIREUM_HOME}" ]; then                      #
   echo "Please set SIREUM_HOME env var"               #
   exit -1                                             #
 fi                                                    #
-exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"    #
+exec "${SIREUM_HOME}/bin/sireum" slang run "$0" "$@"    #
 :BOF
 setlocal
 if not defined SIREUM_HOME (
   echo Please set SIREUM_HOME env var
   exit /B -1
 )
-%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+"%SIREUM_HOME%\bin\sireum.bat" slang run %0 %*
 exit /B %errorlevel%
 ::!#*/
 // #Sireum

isolette/hamr/slang/bin/sergen.cmd

@@ -1,17 +1,17 @@
 ::/*#! 2> /dev/null                                   #
 @ 2>/dev/null # 2>nul & echo off & goto BOF           #
-if [ -z ${SIREUM_HOME} ]; then                        #
+if [ -z "${SIREUM_HOME}" ]; then                      #
   echo "Please set SIREUM_HOME env var"               #
   exit -1                                             #
 fi                                                    #
-exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"    #
+exec "${SIREUM_HOME}/bin/sireum" slang run "$0" "$@"    #
 :BOF
 setlocal
 if not defined SIREUM_HOME (
   echo Please set SIREUM_HOME env var
   exit /B -1
 )
-%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+"%SIREUM_HOME%\bin\sireum.bat" slang run %0 %*
 exit /B %errorlevel%
 ::!#*/
 // #Sireum

isolette/hamr/slang/bin/slangcheck.cmd

@@ -1,17 +1,17 @@
 ::/*#! 2> /dev/null                                   #
 @ 2>/dev/null # 2>nul & echo off & goto BOF           #
-if [ -z ${SIREUM_HOME} ]; then                        #
+if [ -z "${SIREUM_HOME}" ]; then                      #
   echo "Please set SIREUM_HOME env var"               #
   exit -1                                             #
 fi                                                    #
-exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"    #
+exec "${SIREUM_HOME}/bin/sireum" slang run "$0" "$@"    #
 :BOF
 setlocal
 if not defined SIREUM_HOME (
   echo Please set SIREUM_HOME env var
   exit /B -1
 )
-%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+"%SIREUM_HOME%\bin\sireum.bat" slang run %0 %*
 exit /B %errorlevel%
 ::!#*/
 // #Sireum

isolette/hamr/slang/bin/transpile.cmd

@@ -1,17 +1,17 @@
 ::/*#! 2> /dev/null                                   #
 @ 2>/dev/null # 2>nul & echo off & goto BOF           #
-if [ -z ${SIREUM_HOME} ]; then                        #
+if [ -z "${SIREUM_HOME}" ]; then                      #
   echo "Please set SIREUM_HOME env var"               #
   exit -1                                             #
 fi                                                    #
-exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"    #
+exec "${SIREUM_HOME}/bin/sireum" slang run "$0" "$@"    #
 :BOF
 setlocal
 if not defined SIREUM_HOME (
   echo Please set SIREUM_HOME env var
   exit /B -1
 )
-%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+"%SIREUM_HOME%\bin\sireum.bat" slang run %0 %*
 exit /B %errorlevel%
 ::!#*/
 // #Sireum

isolette/hamr/slang/versions.properties

@@ -1,18 +1,19 @@
-org.sireum.slang-embedded-art%%slang-embedded-art%=94cf914
+org.sireum.slang-embedded-art%%slang-embedded-art%=bf6233a
 
 org.sireum%inspector-capabilities%=0.6-SNAPSHOT
 org.sireum%inspector-gui%=0.6-SNAPSHOT
 org.sireum%inspector-services-jvm%=0.6-SNAPSHOT
 
-org.sireum.kekinian%%hamr-vision%=5990efb6ca
 
 # remove the following entries if you want to use the versions
 # that ship with sireum (i.e. $SIREUM_HOME/bin/sireum --version)
 
 # Scala compiler plugin for Slang
-org.sireum%%scalac-plugin%=4.20240329.e93e5db
+org.sireum%%scalac-plugin%=4.20241212.72b1947
 
-org.sireum.kekinian%%library%=5990efb6ca
+org.sireum.kekinian%%library%=d3c137b291
 
-org.scala-lang%scala-library%=2.13.13
-org.scalatest%%scalatest%%=3.2.18
+org.sireum.kekinian%%hamr-vision%=d3c137b291
+
+org.scala-lang%scala-library%=2.13.15
+org.scalatest%%scalatest%%=3.2.19

rts/aadl/bin/run-hamr.cmd

@@ -47,7 +47,8 @@ if(Os.cliArgs.size > 1) {
   Os.exit(1)
 }
 
-val slangOutputDir =  aadlDir.up / "hamr" / "slang"
+val hamrDir =  aadlDir.up / "hamr" 
+val slangOutputDir =  hamrDir / "slang"
 
 val packageName = "RTS"
 
@@ -60,16 +61,16 @@ val platform: String =
 val codegenArgs = ISZ("hamr", "codegen",
   "--platform", platform,
   "--package-name", packageName,
-  "--output-dir", (aadlDir.up / "hamr" / "slang").string,
-  "--output-c-dir", (aadlDir.up / "hamr" / "c").string,
-  "--camkes-output-dir", (aadlDir.up / "hamr" / "camkes").string,  
+  "--output-dir", hamrDir.value,
+  "--output-c-dir", (hamrDir / "c").string,
+  "--sel4-output-dir", (hamrDir / "camkes").string,  
   "--verbose",
   //"--no-proyek-ive",
   "--run-transpiler",
   "--bit-width", "32", 
   "--max-string-size", "256",
   "--max-array-size", "1",
-  "--aadl-root-dir", aadlDir.string,
+  "--workspace-root-dir", aadlDir.string,
   (aadlDir / ".system").string)
 
 val results = Os.proc(osireum ++ codegenArgs).echo.console.run()

rts/hamr/c/bin/compile.cmd

@@ -1,17 +1,17 @@
 ::/*#! 2> /dev/null                                   #
 @ 2>/dev/null # 2>nul & echo off & goto BOF           #
-if [ -z ${SIREUM_HOME} ]; then                       #
+if [ -z "${SIREUM_HOME}" ]; then                     #
   echo "Please set SIREUM_HOME env var"               #
   exit -1                                             #
 fi                                                    #
-exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@" #
+exec "${SIREUM_HOME}/bin/sireum" slang run "$0" "$@" #
 :BOF
 setlocal
 if not defined SIREUM_HOME (
   echo Please set SIREUM_HOME env var
   exit /B -1
 )
-%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+"%SIREUM_HOME%\bin\sireum.bat" slang run %0 %*
 exit /B %errorlevel%
 ::!#*/
 // #Sireum

rts/hamr/c/etc_seL4/adapters/Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator/Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_adapter.c

@@ -3,23 +3,23 @@
 Unit RTS_Actuation_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_adapter_initialiseArchitecture(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_adapter.c", "", "RTS_Actuation_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_adapter_initialiseArchitecture", 0);
 
-  RTS_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_actuator_initialiseArchitecture(SF_LAST);
+  RTS_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_actuator_seL4App_initialiseArchitecture(SF_LAST);
 }
 
 Unit RTS_Actuation_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_adapter_initialiseEntryPoint(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_adapter.c", "", "RTS_Actuation_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_adapter_initialiseEntryPoint", 0);
 
-  RTS_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_actuator_initialiseEntryPoint(SF_LAST);
+  RTS_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_actuator_seL4App_initialiseEntryPoint(SF_LAST);
 }
 
 Unit RTS_Actuation_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_adapter_computeEntryPoint(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_adapter.c", "", "RTS_Actuation_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_adapter_computeEntryPoint", 0);
 
-  RTS_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_actuator_computeEntryPoint(SF_LAST);
+  RTS_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_actuator_seL4App_computeEntryPoint(SF_LAST);
 }
 
 art_Bridge_EntryPoints RTS_Actuation_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_adapter_entryPoints(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_adapter.c", "", "RTS_Actuation_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_adapter_entryPoints", 0);
 
-  return RTS_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_actuator_entryPoints(SF_LAST);
+  return RTS_Actuator_i_actuationSubsystem_saturationActuatorUnit_saturationActuator_actuator_actuator_seL4App_entryPoints(SF_LAST);
 }

rts/hamr/c/etc_seL4/adapters/Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator/Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_adapter.c

@@ -3,23 +3,23 @@
 Unit RTS_Actuation_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_adapter_initialiseArchitecture(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_adapter.c", "", "RTS_Actuation_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_adapter_initialiseArchitecture", 0);
 
-  RTS_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_actuator_initialiseArchitecture(SF_LAST);
+  RTS_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_actuator_seL4App_initialiseArchitecture(SF_LAST);
 }
 
 Unit RTS_Actuation_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_adapter_initialiseEntryPoint(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_adapter.c", "", "RTS_Actuation_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_adapter_initialiseEntryPoint", 0);
 
-  RTS_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_actuator_initialiseEntryPoint(SF_LAST);
+  RTS_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_actuator_seL4App_initialiseEntryPoint(SF_LAST);
 }
 
 Unit RTS_Actuation_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_adapter_computeEntryPoint(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_adapter.c", "", "RTS_Actuation_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_adapter_computeEntryPoint", 0);
 
-  RTS_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_actuator_computeEntryPoint(SF_LAST);
+  RTS_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_actuator_seL4App_computeEntryPoint(SF_LAST);
 }
 
 art_Bridge_EntryPoints RTS_Actuation_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_adapter_entryPoints(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_adapter.c", "", "RTS_Actuation_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_adapter_entryPoints", 0);
 
-  return RTS_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_actuator_entryPoints(SF_LAST);
+  return RTS_Actuator_i_actuationSubsystem_tempPressureActuatorUnit_tempPressureActuator_actuator_actuator_seL4App_entryPoints(SF_LAST);
 }

rts/hamr/c/etc_seL4/adapters/ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread/ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_adapter.c

@@ -3,23 +3,23 @@
 Unit RTS_Actuators_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_adapter_initialiseArchitecture(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_adapter.c", "", "RTS_Actuators_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_adapter_initialiseArchitecture", 0);
 
-  RTS_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_actuatorsMockThread_initialiseArchitecture(SF_LAST);
+  RTS_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_actuatorsMockThread_seL4App_initialiseArchitecture(SF_LAST);
 }
 
 Unit RTS_Actuators_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_adapter_initialiseEntryPoint(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_adapter.c", "", "RTS_Actuators_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_adapter_initialiseEntryPoint", 0);
 
-  RTS_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_actuatorsMockThread_initialiseEntryPoint(SF_LAST);
+  RTS_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_actuatorsMockThread_seL4App_initialiseEntryPoint(SF_LAST);
 }
 
 Unit RTS_Actuators_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_adapter_computeEntryPoint(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_adapter.c", "", "RTS_Actuators_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_adapter_computeEntryPoint", 0);
 
-  RTS_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_actuatorsMockThread_computeEntryPoint(SF_LAST);
+  RTS_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_actuatorsMockThread_seL4App_computeEntryPoint(SF_LAST);
 }
 
 art_Bridge_EntryPoints RTS_Actuators_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_adapter_entryPoints(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_adapter.c", "", "RTS_Actuators_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_adapter_entryPoints", 0);
 
-  return RTS_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_actuatorsMockThread_entryPoints(SF_LAST);
+  return RTS_ActuatorsMockThread_i_actuatorsMock_actuatorsMockThread_actuatorsMockThread_seL4App_entryPoints(SF_LAST);
 }

rts/hamr/c/etc_seL4/adapters/CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic/CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_adapter.c

@@ -3,23 +3,23 @@
 Unit RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_adapter_initialiseArchitecture(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_adapter.c", "", "RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_adapter_initialiseArchitecture", 0);
 
-  RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_coincidenceLogic_initialiseArchitecture(SF_LAST);
+  RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_coincidenceLogic_seL4App_initialiseArchitecture(SF_LAST);
 }
 
 Unit RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_adapter_initialiseEntryPoint(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_adapter.c", "", "RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_adapter_initialiseEntryPoint", 0);
 
-  RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_coincidenceLogic_initialiseEntryPoint(SF_LAST);
+  RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_coincidenceLogic_seL4App_initialiseEntryPoint(SF_LAST);
 }
 
 Unit RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_adapter_computeEntryPoint(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_adapter.c", "", "RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_adapter_computeEntryPoint", 0);
 
-  RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_coincidenceLogic_computeEntryPoint(SF_LAST);
+  RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_coincidenceLogic_seL4App_computeEntryPoint(SF_LAST);
 }
 
 art_Bridge_EntryPoints RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_adapter_entryPoints(STACK_FRAME_ONLY) {
   DeclNewStackFrame(caller, "CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_adapter.c", "", "RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_adapter_entryPoints", 0);
 
-  return RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_coincidenceLogic_entryPoints(SF_LAST);
+  return RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_pressureLogic_coincidenceLogic_coincidenceLogic_seL4App_entryPoints(SF_LAST);
 }