Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
Frama-C Website
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Container Registry
Operate
Environments
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD 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 Website
Commits
fed01928
Commit
fed01928
authored
4 years ago
by
Patrick Baudin
Browse files
Options
Downloads
Patches
Plain Diff
Update acsl-importer.md
parent
e5c75917
No related branches found
Branches containing commit
No related tags found
1 merge request
!47
Adds ACSL importer
Pipeline
#28521
passed
4 years ago
Stage: test
Stage: deploy
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
_fc-plugins/acsl-importer.md
+26
-4
26 additions, 4 deletions
_fc-plugins/acsl-importer.md
with
26 additions
and
4 deletions
_fc-plugins/acsl-importer.md
+
26
−
4
View file @
fed01928
...
...
@@ -8,15 +8,35 @@ distrib_mode: proprietary
## Overview
This plug-in adds to Frama-C support for out of C source files ACSL specification. Therefore
it is useful only to people that intend to write ACSL specifications and do not want to write
them inside comments of the C source files.
The plug-in allows to import external ACSL specifications written in files,
separated from the C source files.
That provides more flexibility in the use of ACSL in the life cycle of
software since the merge between the specifications and the source code is
done by the plug-in.
In addition, the plug-in allows to enter ACSL annotations directly via the Graphical User
Interface.
Therefore
`ACSL Importer`
plug-in is useful only to people that intend to write
ACSL specifications and do not want to write them inside comments of the C source files.
## Usage
The use of the plug-in could be the following, except if the given options lead
to run analysis (analysis should be launched through the graphical interface):
-
`frama-c-gui <importing options> <C files>`
Otherwise, options have to be splitted into two groups and given as follow:
-
`frama-c-gui <importing options> <C files> -then <analysis options>`
Once the plugin installed, the next command gives the up-to-date list of the
plug-in options:
-
`frama-c -acsl-importer-help`
All options of the plug-in are prefixed by
`-acsl-`
.
The main options are:
...
...
@@ -39,6 +59,8 @@ The main options are:
pretty prints a text containing the version ID of the plugin.
## Example
The plug-in can be used as follows. From a C file:
```
c
...
...
@@ -87,7 +109,7 @@ function job:
The following command line:
```
frama
-c -acsl-import demo.acsl demo.c -print -no-unicode
frama-c -acsl-import demo.acsl demo.c -print -no-unicode
```
generates the following output:
...
...
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