Skip to content

Commit

Permalink
update cl args
Browse files Browse the repository at this point in the history
  • Loading branch information
jasonbelt committed Jan 27, 2025
1 parent db35beb commit 9ea82b6
Show file tree
Hide file tree
Showing 420 changed files with 2,379 additions and 20,121 deletions.
2 changes: 2 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
**/.aadlbin-gen/
**/.metals/
**/.vscode/
**/instances
**/c/nix
**/*-build/
Expand Down
6 changes: 3 additions & 3 deletions aadl/aadl/bin/run-hamr.cmd
Original file line number Diff line number Diff line change
Expand Up @@ -58,15 +58,15 @@ val excludeComponentImpl = F
var 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,
"--camkes-output-dir", (aadlDir.up / "hamr" / "camkes").string,
"--sel4-output-dir", (aadlDir.up / "hamr" / "camkes").string,
"--run-transpiler",
"--bit-width", "32",
"--max-string-size", "256",
"--max-array-size", "1",
"--verbose",
"--aadl-root-dir", aadlDir.string)
"--workspace-root-dir", aadlDir.string)

if (platform == "JVM") {
codegenArgs = codegenArgs :+ "--runtime-monitoring"
Expand Down
6 changes: 3 additions & 3 deletions aadl/hamr/c/bin/compile.cmd
Original file line number Diff line number Diff line change
@@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Original file line number Diff line number Diff line change
Expand Up @@ -3,23 +3,23 @@
Unit RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_adapter_initialiseArchitecture(STACK_FRAME_ONLY) {
DeclNewStackFrame(caller, "CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_adapter.c", "", "RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_adapter_initialiseArchitecture", 0);

RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_coincidenceLogic_initialiseArchitecture(SF_LAST);
RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_coincidenceLogic_seL4App_initialiseArchitecture(SF_LAST);
}

Unit RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_adapter_initialiseEntryPoint(STACK_FRAME_ONLY) {
DeclNewStackFrame(caller, "CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_adapter.c", "", "RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_adapter_initialiseEntryPoint", 0);

RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_coincidenceLogic_initialiseEntryPoint(SF_LAST);
RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_coincidenceLogic_seL4App_initialiseEntryPoint(SF_LAST);
}

Unit RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_adapter_computeEntryPoint(STACK_FRAME_ONLY) {
DeclNewStackFrame(caller, "CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_adapter.c", "", "RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_adapter_computeEntryPoint", 0);

RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_coincidenceLogic_computeEntryPoint(SF_LAST);
RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_coincidenceLogic_seL4App_computeEntryPoint(SF_LAST);
}

art_Bridge_EntryPoints RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_adapter_entryPoints(STACK_FRAME_ONLY) {
DeclNewStackFrame(caller, "CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_adapter.c", "", "RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_adapter_entryPoints", 0);

return RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_coincidenceLogic_entryPoints(SF_LAST);
return RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_saturationLogic_coincidenceLogic_coincidenceLogic_seL4App_entryPoints(SF_LAST);
}
Original file line number Diff line number Diff line change
Expand Up @@ -3,23 +3,23 @@
Unit RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_adapter_initialiseArchitecture(STACK_FRAME_ONLY) {
DeclNewStackFrame(caller, "CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_adapter.c", "", "RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_adapter_initialiseArchitecture", 0);

RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_coincidenceLogic_initialiseArchitecture(SF_LAST);
RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_coincidenceLogic_seL4App_initialiseArchitecture(SF_LAST);
}

Unit RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_adapter_initialiseEntryPoint(STACK_FRAME_ONLY) {
DeclNewStackFrame(caller, "CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_adapter.c", "", "RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_adapter_initialiseEntryPoint", 0);

RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_coincidenceLogic_initialiseEntryPoint(SF_LAST);
RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_coincidenceLogic_seL4App_initialiseEntryPoint(SF_LAST);
}

Unit RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_adapter_computeEntryPoint(STACK_FRAME_ONLY) {
DeclNewStackFrame(caller, "CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_adapter.c", "", "RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_adapter_computeEntryPoint", 0);

RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_coincidenceLogic_computeEntryPoint(SF_LAST);
RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_coincidenceLogic_seL4App_computeEntryPoint(SF_LAST);
}

art_Bridge_EntryPoints RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_adapter_entryPoints(STACK_FRAME_ONLY) {
DeclNewStackFrame(caller, "CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_adapter.c", "", "RTS_Actuation_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_adapter_entryPoints", 0);

return RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_coincidenceLogic_entryPoints(SF_LAST);
return RTS_CoincidenceLogic_i_actuationSubsystem_actuationUnit1_temperatureLogic_coincidenceLogic_coincidenceLogic_seL4App_entryPoints(SF_LAST);
}
Loading

0 comments on commit 9ea82b6

Please sign in to comment.