Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
meta
Commits
4c29c7bb
Commit
4c29c7bb
authored
Nov 05, 2020
by
Virgile Prevosto
Browse files
shorter option name for separating annotations + update README
parent
1815c5ce
Changes
3
Hide whitespace changes
Inline
Side-by-side
README.md
View file @
4c29c7bb
...
...
@@ -31,6 +31,11 @@ generated from a given meta-property. This name is of the form `_nnn`, where `nn
is unique within each annotated function. Hence, with this option, each generated
`meta`
assertion
is identified uniquely by the
`property_name`
, the function to which it belongs, and this id.
Finally, generated annotations are normally tied to the statement upon which
they apply. Option
`-meta-separate-annots`
will generate no-op instructions and
tie each annotation to a separate instruction, forcing the order in which they
ought to be considered.
Several other options are available: use
`frama-c -meta-h`
for more information.
## Basic meta-property
...
...
meta_options.ml
View file @
4c29c7bb
...
...
@@ -89,7 +89,7 @@ module Static_bindings = Self.Int (struct
end
)
module
Separate_annots
=
Self
.
False
(
struct
let
option_name
=
"-meta-separate-annot
-instruction
"
let
option_name
=
"-meta-separate-annot
s
"
let
help
=
"When set, each generated statement annotation will be tied to its own \
(nop) instruction. Otherwise (default), all annotations generated for \
...
...
tests/meta/number_assertions.c
View file @
4c29c7bb
/* run.config
OPT: @META@ -meta-number-assertions @PRINT@
OPT: @META@ -kernel-verbose 0 -meta-separate-annot
-instruction
@PRINT@
OPT: @META@ -kernel-verbose 0 -meta-separate-annot
s
@PRINT@
*/
int
*
p1
;
...
...
Write
Preview
Supports
Markdown
0%
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!
Cancel
Please
register
or
sign in
to comment