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
0798956a
Commit
0798956a
authored
2 years ago
by
Patrick Baudin
Committed by
François Bobot
2 years ago
Browse files
Options
Downloads
Patches
Plain Diff
[Scripts] adds some commands: init, build and install
parent
f82dd3e1
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
bin/frama-c-build-scripts.sh
+58
-15
58 additions, 15 deletions
bin/frama-c-build-scripts.sh
with
58 additions
and
15 deletions
bin/frama-c-build-scripts.sh
+
58
−
15
View file @
0798956a
...
@@ -23,11 +23,18 @@
...
@@ -23,11 +23,18 @@
PACKAGE
=
"frama-c-scripts"
PACKAGE
=
"frama-c-scripts"
CMD
=
"init"
THIS_SCRIPT
=
"
$0
"
THIS_SCRIPT
=
"
$0
"
Usage
()
{
Usage
()
{
echo
"Usage:
$(
basename
${
THIS_SCRIPT
}
)
<script-dir> [<modules>]"
echo
"Usage:
$(
basename
${
THIS_SCRIPT
}
)
[<CMD>] <script-dir> [<modules>]"
echo
" Build a script library to be used by Frama-C kernel"
echo
" Build a script library to be used by Frama-C kernel."
echo
""
echo
"Commands:"
echo
"- init: generates dune files (default command)"
echo
"- build: performs the compilation of the script libraries via
\"
dune build @install
\"
"
echo
"- install: performs the installation of the script libraries via
\"
dune install
\"
"
echo
""
echo
"Arguments"
echo
"Arguments"
echo
" <script-dir>: directory that contents the script files:"
echo
" <script-dir>: directory that contents the script files:"
echo
" - the basename of this directory fixes the name of the script library:
${
PACKAGE
}
.<basename>"
echo
" - the basename of this directory fixes the name of the script library:
${
PACKAGE
}
.<basename>"
...
@@ -43,6 +50,14 @@ Error () {
...
@@ -43,6 +50,14 @@ Error () {
exit
1
exit
1
}
}
###############
# Command line processing
case
"
$1
"
in
"init"
|
"build"
|
"install"
)
CMD
=
"
$1
"
;
shift
;;
*
)
;;
esac
[
"
$1
"
!=
""
]
||
Error
"Missing argument: no script directory"
[
"
$1
"
!=
""
]
||
Error
"Missing argument: no script directory"
[
"
$1
"
!=
"-h"
]
||
Usage
[
"
$1
"
!=
"-h"
]
||
Usage
[
"
$1
"
!=
"-help"
]
||
Usage
[
"
$1
"
!=
"-help"
]
||
Usage
...
@@ -93,7 +108,7 @@ GenerateFile () {
...
@@ -93,7 +108,7 @@ GenerateFile () {
if
[
-e
"
$2
"
]
;
then
if
[
-e
"
$2
"
]
;
then
echo
"
$1
file exists already:
$2
"
echo
"
$1
file exists already:
$2
"
else
else
echo
"-
Generate
$1
file:
$2
"
echo
"-
Creating
$1
file:
$2
"
$1
|
while
read
p
;
do
$1
|
while
read
p
;
do
echo
"
$p
"
>>
"
$2
"
echo
"
$p
"
>>
"
$2
"
done
done
...
@@ -112,28 +127,56 @@ esac
...
@@ -112,28 +127,56 @@ esac
###############
###############
EchoDuneCmd
()
{
if
[
"
${
DUNE_PROJECT_DIR
}
"
=
"."
]
;
then
echo
" >
$@
"
else
echo
" > (cd
${
DUNE_PROJECT_DIR
}
&&
$@
)"
fi
}
DuneBuild
()
{
echo
""
echo
"- Compiling the script library
\"
${
PACKAGE
}
.
${
SCRIPT_NAME
}
\"
via
\"
dune build @install
\"
command..."
dune build @install
[
"
$?
"
=
"0"
]
||
Error
"the compilation fails!"
}
DuneInstall
()
{
echo
""
echo
"- Install the script library
\"
${
PACKAGE
}
.
${
SCRIPT_NAME
}
\"
via
\"
dune install
\"
command..."
dune
install
}
###############
[
"
$(
basename
"
${
DUNE_FILE
}
"
)
"
=
"dune"
]
||
Error
"Wrong basename for a dune file:
${
DUNE_FILE
}
"
[
"
$(
basename
"
${
DUNE_FILE
}
"
)
"
=
"dune"
]
||
Error
"Wrong basename for a dune file:
${
DUNE_FILE
}
"
[
"
$(
basename
"
${
DUNE_PROJECT
}
"
)
"
=
"dune-project"
]
||
Error
"Wrong basename for a dune-project file:
${
DUNE_PROJECT
}
"
[
"
$(
basename
"
${
DUNE_PROJECT
}
"
)
"
=
"dune-project"
]
||
Error
"Wrong basename for a dune-project file:
${
DUNE_PROJECT
}
"
GenerateFile Dune
"
${
DUNE_FILE
}
"
GenerateFile DuneProject
"
${
DUNE_PROJECT
}
"
GenerateFile DuneProject
"
${
DUNE_PROJECT
}
"
GenerateFile Dune
"
${
DUNE_FILE
}
"
EchoDuneCmd
()
if
[
"
$CMD
"
=
"init"
]
;
then
if
[
"
${
DUNE_PROJECT_DIR
}
"
=
"."
]
;
then
echo
""
echo
" >
$@
"
echo
"To compile the all scripts defined inside this 'dune project'
\"
${
PACKAGE
}
\"
, runs the following command:"
EchoDuneCmd
"dune build @install"
else
else
echo
" > (cd
${
DUNE_PROJECT_DIR
}
&&
$@
)"
DuneBuild
fi
fi
echo
""
echo
"To compile the all scripts defined inside this 'dune project'
\"
${
PACKAGE
}
\"
, runs the following command:"
echo
"So, the script libraries, are compiled and installed into the local '_build' directory."
EchoDuneCmd
"dune build @install"
echo
"That also create or update the 'opam' file
\"
${
PACKAGE
}
.opam
\"
allowing a global installation of all script libraries."
echo
"So, the script libraries, are installed into the local '_build' directory."
echo
"That also generate the 'opam' file
\"
${
PACKAGE
}
.opam
\"
allowing a global installation of all script libraries."
echo
""
echo
""
echo
"To load this script library from Frama-C, runs the following command:"
echo
"To load this script library from Frama-C, runs the following command:"
EchoDuneCmd
"dune exec -- frama-c -load-library
${
PACKAGE
}
.
${
SCRIPT_NAME
}
..."
EchoDuneCmd
"dune exec -- frama-c -load-library
${
PACKAGE
}
.
${
SCRIPT_NAME
}
..."
if
[
"
$CMD
"
=
"install"
]
;
then
DuneInstall
else
echo
""
echo
"All libraries of this 'dune project'
\"
${
PACKAGE
}
\"
can also be installed via 'dune' using from the generated 'opam' file:
\"
${
PACKAGE
}
.opam
\"
"
EchoDuneCmd
"dune install"
fi
echo
""
echo
""
echo
"All libraries of this 'dune project'
\"
${
PACKAGE
}
\"
can also be installed via 'dune' using from the generated 'opam' file:
\"
${
PACKAGE
}
.opam
\"
"
EchoDuneCmd
"dune install"
echo
"Then, this script library can directly be loaded by Frama-C from the following command:"
echo
"Then, this script library can directly be loaded by Frama-C from the following command:"
echo
" > frama-c -load-library
${
PACKAGE
}
.
${
SCRIPT_NAME
}
..."
echo
" > frama-c -load-library
${
PACKAGE
}
.
${
SCRIPT_NAME
}
..."
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