INSTALL

			   -------------------------
			   INSTALLATION INSTRUCTIONS
			   -------------------------

===============================================================================
				    SUMMARY
===============================================================================

0)  Summary
1)  Quick Start
2)  Requirements
3)  Configuration
4)  Compilation
5)  Installation
6)  Custom Installation
7)  Testing the Installation
8)  Uninstallation
9)  Have Fun with E-ACSL!

===============================================================================
				  QUICK START
===============================================================================

1) Install Frama-C if not already installed.

2a) On Linux-like distribution:
  ./configure && make && sudo make install

2b) On Windows+Cygwin or Windows+MinGW+msys:
  ./configure --prefix C:/windows/path/with/direct/slash && make && make install

4) Optionally, test your installation by running:
   frama-c.byte -e-acsl tests/runtime/true.i -then-on e-acsl -print
   frama-c -e-acsl tests/runtime/true.i -then-on e-acsl -print

See below for more detailed and specific instructions.

===============================================================================
				  REQUIREMENTS
===============================================================================

- Frama-C = Magnesium-20151002
  (no warranty that this plug-in works with a more recent version of Frama-C)

- The native version of the plug-in is only available if native dynamic linking
  feature of OCaml is available on your system (see Frama-C User Manual,
  Section 3.1).
- Optionally, the GMP library >= 4.3
  It is required to run the tests and to run some generated programs,
  but not to run the plug-in through Frama-C.

===============================================================================
				 CONFIGURATION
===============================================================================

The E-ACSL plug-in is configured by "./configure [options]"

configure is generated by autoconf, so that the standard options for setting
installation directories are available, in particular '--prefix=/path'.

Under Cygwin or MinGW:
----------------------
Use "./configure --prefix C:/windows/path/with/direct/slash".

===============================================================================
				  COMPILATION
===============================================================================

Type "make".

Makefile targets of interest are:
- doc	   generates the API documentation

===============================================================================
				  INSTALLATION
===============================================================================

Type "make install"
(depending on the installation directory, may require superuser privileges).

It is possible to install in a given directory by setting
the DESTDIR variable: "make install DESTDIR=/tmp" installs Frama-C in
sub-directories of /tmp.

The following files are installed.

Object files: (usually in `frama-c -print-plugin-path`)
-------------
- E_ACSL.cmi
- E_ACSL.cmo
- E_ACSL.cmxs (only if native dynamic linking of OCaml is available)

Shared files: (usually in `frama-c -print-share-path`/e-acsl)
-------------
- e_acsl_assert.h
- e_acsl_debug.h
- e_acsl_gmp.h
- e_acsl_gmp_types.h
- e_acsl.h
- e_acsl_mmodel.h
- e_acsl_printf.h
- e_acsl_string.h
- e_acsl_syscall.h
- glibc/memcpy.c
- glibc/wordcopy.c
- glibc/strncmp.c
- glibc/memcopy.h
- glibc/pagecopy.h
- glibc/strlen.c
- glibc/memmove.c
- glibc/memset.c
- glibc/strcmp.c
- bittree_model/e_acsl_bittree_api.h
- bittree_model/e_acsl_bittree.h
- bittree_model/e_acsl_bittree_mmodel.c

Manuals: (usually in `frama-c -print-share-path`/manuals)
--------
- e-acsl.pdf
- e-acsl-implementation.pdf
- e-acsl-manual.pdf

===============================================================================
			      CUSTOM INSTALLATION
===============================================================================

You can manually move any installed files. However, in such a case, you have to
set specific environment variables in order that Frama-C found the appropriate
objects when required.

The environment variables are:
------------------------------
FRAMAC_SHARE: absolute path to the Frama-C share subdirectory
FRAMAC_LIB: absolute path of the Frama-C lib subdirectory
FRAMAC_PLUGIN: absolute path of the Frama-C plug-in directory.

===============================================================================
			    TESTING THE INSTALLATION
===============================================================================

This step is optional.

Test your installation by running:
  frama-c.byte -e-acsl tests/runtime/true.i -then-on e-acsl -print
  frama-c -e-acsl tests/runtime/true.i -then-on e-acsl -print

The second command only works if native dynamic linking of OCaml is available
on your system.

===============================================================================
				 UNINSTALLATION
===============================================================================

Type "make uninstall" to remove Frama-C and all the installed plug-ins.
That works only if you have not manually moved the installed files (see Section
"Custom Installation").

===============================================================================
			     HAVE FUN WITH E-ACSL!
===============================================================================