Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
a5f8de10
Commit
a5f8de10
authored
6 months ago
by
Allan Blanchard
Browse files
Options
Downloads
Patches
Plain Diff
[release] add Ivette packages
parent
0b501e05
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
.gitlab-ci.yml
+2
-2
2 additions, 2 deletions
.gitlab-ci.yml
INSTALL.md
+49
-0
49 additions, 0 deletions
INSTALL.md
dev/build-release.sh
+67
-23
67 additions, 23 deletions
dev/build-release.sh
with
118 additions
and
25 deletions
.gitlab-ci.yml
+
2
−
2
View file @
a5f8de10
...
...
@@ -343,8 +343,8 @@ build-ivette-macos-packages:
-
opam switch create --empty .
-
eval $(opam env --switch=. --set-switch)
-
opam pin . -n -k path
-
opam install headache
-
opam install --jobs 2 --deps-only .
-
opam install headache
-y
-
opam install --jobs 2 --deps-only .
-y
# Build Frama-C API
-
dune build -j2 @install
-
make -C ivette api
...
...
This diff is collapsed.
Click to expand it.
INSTALL.md
+
49
−
0
View file @
a5f8de10
...
...
@@ -8,6 +8,9 @@
-
[
Installing Custom Versions of Frama-C
](
#installing-custom-versions-of-frama-c
)
-
[
Installing Frama-C on Windows via WSL
](
#installing-frama-c-on-windows-via-wsl
)
-
[
Installing Frama-C on macOS
](
#installing-frama-c-on-macos
)
-
[
Installing Ivette via the online packages
](
#installing-ivette-via-the-online-packages
)
-
[
On Linux
](
#installing-ivette-via-the-online-packages-on-linux
)
-
[
On macOS
](
#installing-ivette-via-the-online-packages-on-macos
)
-
[
Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)
](
#installing-frama-c-via-your-linux-distribution-debianubuntufedora
)
-
[
Compiling from source
](
#compiling-from-source
)
-
[
Quick Start
](
#quick-start
)
...
...
@@ -300,6 +303,52 @@ We highly recommend to rely on it for the installation of Frama-C.
Instructions on installing and running it are presented by opam when
the
`frama-c`
package is installed. Follow them to get Ivette running.
## Installing Ivette via the online packages
**Warning:**
if you already have an
`ivette`
script along with
`frama-c`
, that
script is used for bootstrapping the installation of Ivette from source through
your internet connection. The instructions provided here are intended to
_replace_
the installation procedure from source. Hence, it is highly
recommended for you to remove the bootstrapping
`ivette`
script if you want to
use the binary distribution of Ivette.
Only stable distributions are available online for now.
Download the Ivette distribution that corresponds to your version of Frama-C.
### Installing Ivette via the online packages on Linux
Requirement: libfuse2 must be installed.
Download the binary distribution (for now, only x86-64 and ARM64 are supported).
Install it wherever you want:
```
sh
cp
frama-c-ivette-linux-<
arch
>
-<version>.AppImage <IVETTE-INSTALL-PATH>/ivette.AppImage
```
Then add an alias
`ivette`
that just runs the AppImage:
```
sh
alias
ivette
=
<ABSOLUTE-IVETTE-INSTALL-PATH>/ivette.AppImage
```
### Installing Ivette via the online packages on macOS
Download the universal binary distribution of Ivette and install it, typically
in
`/Applications/Ivette.app`
. To launch Ivette from the command line, you will
need your own
`ivette`
script, like the following one:
```
sh
#! /usr/bin/env sh
exec
open
-na
<IVETTE-INSTALL>/Ivette.app
--args
\
--command
<FRAMAC-INSTALL>/frama-c
\
--working
$PWD
$*
```
Simply replace
`<IVETTE-INSTALL>`
and
`<FRAMAC-INSTALL>`
in the code above with
the (absolute) paths to your
`Ivette.app`
and
`frama-c`
binaries,
respectively. Then, make your
`ivette`
script executable and simply use it like
the
`frama-c`
command-line binary!
## Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)
...
...
This diff is collapsed.
Click to expand it.
dev/build-release.sh
+
67
−
23
View file @
a5f8de10
...
...
@@ -27,6 +27,9 @@
# Thus, it expects to be run from the root of the Frama-C directory and that
# some CI artifacts are available. Namely:
# - 'frama-c.tar.gz'
# - 'frama-c-ivette-linux-ARM64.AppImage'
# - 'frama-c-ivette-linux-x86-64.AppImage'
# - 'frama-c-ivette-macos-universal.dmg'
# - 'api' directory (with api archives inside)
# - 'manuals' directory (with all manuals incl. acsl + version text files)
# Availability of the files is checked when the script starts. The script also
...
...
@@ -160,6 +163,18 @@ for file in "${API_FILES[@]}"; do
prepare_file
"
$API_DIR
/
$file
-api.tar.gz"
done
show_step
"Searching for Ivette packages"
IVETTE
=(
"frama-c-ivette-linux-ARM64.AppImage"
"frama-c-ivette-linux-x86-64.AppImage"
"frama-c-ivette-macos-universal.dmg"
)
for
package
in
"
${
IVETTE
[@]
}
"
;
do
prepare_file
"
$package
"
done
show_step
"Searching for manuals"
MANUALS
=(
...
...
@@ -237,6 +252,12 @@ function copy_manual_e_acsl {
cp
"
$MANUALS_DIR
/
$1
.
$2
"
"
$EACSL_TARGET_DIR
/
$(
version_name
"
$1
"
)
.
$2
"
}
function
copy_ivette_package
{
name
=
"
${
1
%%.*
}
"
ext
=
"
${
1
#*.
}
"
cp
"
$1
"
"
$PKGS_TARGET_DIR
/
$(
version_name
"
$name
"
)
.
$ext
"
}
function
copy_api
{
if
[
"
$FINAL_RELEASE
"
=
"yes"
]
;
then
cp
"
$API_DIR
/
$1
-api.
$2
"
"
$MANS_TARGET_DIR
/
$1
-api.
$2
"
...
...
@@ -258,15 +279,18 @@ function copy_files {
for
api
in
"
${
API_FILES
[@]
}
"
;
do
copy_api
"
$api
"
"tar.gz"
done
for
package
in
"
${
IVETTE
[@]
}
"
;
do
copy_ivette_package
"
$package
"
done
# Eva has an old manual name that might be in use:
if
[
"
$FINAL_RELEASE
"
=
"yes"
]
;
then
cp
"
$MANS_TARGET_DIR
/frama-c-eva-manual.pdf"
"
$MANS_TARGET_DIR
/frama-c-value-analysis.pdf"
fi
cp
$TARGZ_BASE
"
$
GZ
_TARGET_DIR
/
$TARGZ_VERSION
"
cp
$TARGZ_BASE
"
$
PKGS
_TARGET_DIR
/
$TARGZ_VERSION
"
if
[
"
$FINAL_RELEASE
"
=
"yes"
]
;
then
cp
$TARGZ_BASE
"
$
GZ
_TARGET_DIR
/
$TARGZ_GENERIC
"
cp
$TARGZ_BASE
"
$
PKGS
_TARGET_DIR
/
$TARGZ_GENERIC
"
fi
}
...
...
@@ -338,6 +362,13 @@ for archive in "${COMPANIONS[@]}"; do
echo
"- [
$archive
](
$FRAMAC_COM_DOWNLOAD
/
$NAME
.tar.gz)"
>>
$WIKI_PAGE
done
echo
""
>>
$WIKI_PAGE
echo
"## Ivette packages"
>>
$WIKI_PAGE
for
package
in
"
${
IVETTE
[@]
}
"
;
do
NAME
=
"
${
package
%%.*
}
"
EXT
=
"
${
package
#*.
}
"
echo
"- [
$NAME
](
$FRAMAC_COM_DOWNLOAD
/
$(
version_name
$NAME
)
.
$EXT
)"
>>
$WIKI_PAGE
done
echo
""
>>
$WIKI_PAGE
echo
"## Main changes"
>>
$WIKI_PAGE
sed
's/\(\#.*\)/##\1/'
$CHANGES
>>
$WIKI_PAGE
...
...
@@ -371,6 +402,21 @@ cat >$JSON_DATA <<EOL
"name": "Official source archive",
"url": "https://frama-c.com/download/
$TARGZ_VERSION
",
"link_type":"other"
},
{
"name": "Ivette (Linux ARM64)",
"url": "https://frama-c.com/download/frama-c-ivette-linux-ARM64-
$VERSION_AND_CODENAME
.AppImage",
"link_type":"other"
},
{
"name": "Ivette (Linux x86-64)",
"url": "https://frama-c.com/download/frama-c-ivette-linux-x86-64-
$VERSION_AND_CODENAME
.AppImage",
"link_type":"other"
},
{
"name": "Ivette (macOS universal)",
"url": "https://frama-c.com/download/frama-c-ivette-macos-universal-
$VERSION_AND_CODENAME
.dmg",
"link_type":"other"
}
]
},
...
...
@@ -387,7 +433,6 @@ show_step "Building website"
WEBSITE_DIR
=
"./website"
WEBSITE_DL_DIR
=
"
$WEBSITE_DIR
/download"
WEBSITE_INST_DIR
=
"
$WEBSITE_DIR
/html/installations"
WEBSITE_EVENTS_DIR
=
"
$WEBSITE_DIR
/_events"
WEBSITE_VERSIONS_DIR
=
"
$WEBSITE_DIR
/_fc-versions"
...
...
@@ -398,31 +443,13 @@ mkdir -p $WEBSITE_DIR
mkdir
-p
$WEBSITE_DL_DIR
mkdir
-p
$WEBSITE_DL_DIR
/e-acsl
GZ
_TARGET_DIR
=
$WEBSITE_DL_DIR
PKGS
_TARGET_DIR
=
$WEBSITE_DL_DIR
MANS_TARGET_DIR
=
$WEBSITE_DL_DIR
copy_files
echo
"Download directory built"
# Install
mkdir
-p
$WEBSITE_INST_DIR
INSTALL_WEBPAGE
=
"
$WEBSITE_INST_DIR
/
$LOWER_CODENAME
.md"
EXT
=
"
$CODENAME
(released on
$(
date
+%Y-%m-%d
)
)"
cat
>
$INSTALL_WEBPAGE
<<
EOL
---
layout: installation_page
version:
$LOWER_CODENAME
title: Installation instructions for Frama-C
$VERSION
(
$CODENAME
)
---
EOL
sed
./INSTALL.md
-e
"s/^
\(
# Installing Frama-C
\)
$/
\1
$EXT
/"
>>
$INSTALL_WEBPAGE
echo
"Installation file built"
# Event
mkdir
-p
$WEBSITE_EVENTS_DIR
...
...
@@ -469,6 +496,9 @@ else
ACSL_OR_BETA
=
"acsl:
$ACSL_VERSION_WEBSITE
"
fi
INSTALL_WEBPAGE
=
"https://git.frama-c.com/pub/frama-c/-/blob/
$TAG
/INSTALL.md"
IVETTE_INSTALL
=
"
$INSTALL_WEBPAGE
#installing-ivette-via-the-online-packages-on-"
cat
>
$VERSION_WEBPAGE
<<
EOL
---
layout: version
...
...
@@ -483,7 +513,7 @@ releases:
- name: Source distribution
link: /download/
$TARGZ_VERSION
help: Compilation instructions
help_link:
https://git.frama-c.com/pub/frama-c/-/blob/
$TAG
/INSTALL.md
help_link:
$INSTALL_WEBPAGE
- name: User manual
link: /download/user-manual-
$VERSION_AND_CODENAME
.pdf
- name: Plug-in development guide
...
...
@@ -513,6 +543,20 @@ releases:
link: /download/wp-manual-
$VERSION_AND_CODENAME
.pdf
- name: E-ACSL manual
link: /download/e-acsl/e-acsl-manual-
$VERSION_AND_CODENAME
.pdf
- name: Ivette Packages (experimental)
files:
- name: Linux x86-64 AppImage
link: /download/frama-c-ivette-linux-x86-64-
$VERSION_AND_CODENAME
.AppImage
help: Installation instructions
help_link:
${
IVETTE_INSTALL
}
linux
- name: Linux ARM64 AppImage
link: /download/frama-c-ivette-linux-ARM64-
$VERSION_AND_CODENAME
.AppImage
help: Installation instructions
help_link:
${
IVETTE_INSTALL
}
linux
- name: macOS universal
link: /download/frama-c-ivette-macOS-universal-
$VERSION_AND_CODENAME
.dmg
help: Installation instructions
help_link:
${
IVETTE_INSTALL
}
macos
---
EOL
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment