Skip to content

Mac OS installation Summary

Jump to bottom
Shuanglong Kan edited this page Nov 17, 2022 · 5 revisions

Installing Ultimate on Mac OS:

You must install Ultimate following the step on the page Ultimate Installation When you encounter problems, you can read the following to find solutions.

Ultimate contains a collection of projects; these projects may depend on:

  • other projects in Ultimate,
  • external libraries.

External libraries are loaded by the configuration file: Ultimate_E4.17_JAVA11_*.target (* denotes the corresponding platform: Windows, Linux, and OSX) in the project BA_SiteRepository. Therefore, you must load the target platform before compiling all the projects.

During the compilation, you may encounter the following problems:

1. Incompatible java version.

The error messages could be:

  1. class file has the wrong version 55.0, should be 52.0
  2. Some data types are not supported by current Java version

The reason for these errors is probably the inconsistency of java versions in different projects. You may find that in some projects' MANIFEST.MF, the value of JavaSE is set to 1.8 instead of 11. In my case, eclipse automatically selects Java 1.8 compiler instead of Java 11 compiler. The best way is to check whether all the projects are compiled under Java 11 compiler.

You can do it by:

  1. right-click a project
  2. select Properties
  3. click Java compiler
  4. Check the correctness of the compiler version.

!!You must make sure all projects are compiled under the same Java Compiler!!

2. Fail to generate Lexer and Parser

As Ultimate can accept many different input languages, such as Boogie, SMT, and C. It contains some code using flex and bison to automatically generate java files. For instance, in the project BoogiePLParser, the package de.uni_freiburg.informatik.ultimate.boogie.parser contains a file called Boogie.flex, which is used to generate the lexer file of Boogie language. These Lexer and Parser files may fail to be generated during the compilation and you may have the following compiling problems:

  • Lexer cannot be resolved a data type
  • LanguageExpression cannot be resolved a data type
  • ......

The solution is to refresh the project to make it rebuild. If you have no idea which project fails to generate parser files just to refresh all projects. Pay attention to the project Croccotta, in my case, it always fail to compile at the first compilation. After refreshing the project Croccotta, the compiling errors are solved.

3. Fail to load an eclipse application

After you successfully make all projects in Ultimate compiled, in macOS, you still cannot start the eclipse application. In order to address it. Do the following steps:

Click Run -> Run Configurations -> Plug-ins -> search the plugin-in org.eclipse.swt.cocoa.macosx.x86_64 and select it -> Run.

Clone this wiki locally