Skip to content

MS Windows, MinGW/MSYS environment / Dynamic plugins detection broken when compiling Frama-C from source

ID0001087: This issue was created automatically from Mantis Issue 1087. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0001087 Frama-C Kernel public 2012-02-09 2012-02-16
Reporter sylvain nahas Assigned To monate Resolution fixed
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Nitrogen-20111001 Target Version - Fixed in Version -

Description :

I have compiled and installed Frama-C from source with MinGW, specifying the installation path with --prefix to ./configure.

Configuration, compilation and installation runs OK.

$ frama-c -print-plugin-path returns the correct result.

Still, the program fails to detect the installed dynamic plugins. For example, $frama-c -help does not list the plugins as expected.

It works OK when the environment variable FRAMAC_PLUGIN is set.

Additional Information :

How to reproduce

Install MS Windows SP3.

  1. Install MinGW from here (chose developer installation) ftp://ftp.ntua.gr/mirror/mingw/Installer/mingw-get-inst/mingw-get-inst-20110802/ be sure to follow the instructions from there: http://www.mingw.org/wiki/Getting_Started
  2. Install ocaml http://protz.github.com/ocaml-installer/
  3. Download Frama-C source code: http://frama-c.com/download/frama-c-Nitrogen-20111001.tar.gz
  4. decompress for ex. in C:\Documents\frama-c-Nitrogen
  5. Open the MinGW console and cd in the directory where you decompressed the source $ cd /c/Documents/frama-c-Nitrogen
  6. Configure the source, especially the place where you want to install your program for me: $ ./configure --prefix=/c/Programme/frama-c-Nitrogen
  7. Check the configure output. You should get warning that theorem provers and graphical interface are missing, but no other warnings.
  8. Build and install: $ make && make install

Expected results

$ frama-c -help should list "report", "aorai", "wp" among others as available plugins

Actual results

  1. These plugins are unknown.
  2. The command line: $ FRAMAC_PLUGIN=/install/path/lib/frama-c/plugins frama-c -help shows the expected result
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information