sireum / kekinian

Sireum: A High Assurance System Engineering Platform
http://sireum.org
BSD 2-Clause "Simplified" License
9 stars 2 forks source link

HAMR does not build for ARM64 target #5

Closed podhrmic closed 1 month ago

podhrmic commented 1 month ago

Hello @jasonbelt !

We are attempting to build a ARM64 docker image with FMIDE + HAMR, because a lot of folks at Galois are not using M1/M2 Macs.

Sireum installs just fine for ARM64, but when I attempt to run:

RUN ${SIREUM_HOME}/bin/install/fmide.cmd --verbose

I get the following error:

11 [ 7/10] RUN /opt/Sireum/bin/install/fmide.cmd --verbose
#11 3.526 FMIDE is based on OSATE v2.10.x however ARM architectures require OSATE 2.11+. Sireum Phantom can be used
#11 3.526 to install the Sireum OSATE plugins into a more recent version of OSATE. For more information invoke
#11 3.526 

What would it take to upgrade HAMR to work with OSATE 2.11+ (ideally OSATE 2.12)?

jasonbelt commented 1 month ago

HAMR Phantom can be used to install/update the Sireum OSATE plugins (e.g. HAMR) into an OSATE distribution. You'd need to use OSATE 2.11 or newer when on ARM. For example

${SIREUM_HOME}/bin/sireum hamr phantom --verbose --update --osate /Applications/osate.app

is an example of calling Phantom on an Apple Silicon machine. If the --osate option doesn't exist then OSATE 2.14 will be downloaded and installed at that location, otherwise Phantom will update the Sireum plugins in the existing installation.

Note that the other CASE plugins installed by fmide.cmd (e.g. BriefCASE) are not installed by Phantom, though Phantom could be used if you can provide it the versions of those plugins that have been updated to support OSATE 2.11+.

podhrmic commented 1 month ago

Thanks, that is helpful! Can I tell Phantom to update OSATE to a specific version, e.g. the 2.12 (instead of 2.14)?

jasonbelt commented 1 month ago

You'd first have to manually download and install OSATE 2.12 and then point Phantom at that via the --osate option

podhrmic commented 1 month ago

That worked, thank you!