Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2069
Closed
Open
Issue created Feb 09, 2012 by mantis-gitlab-migration@mantis-gitlab-migration

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
Assignee
Assign to
Time tracking