Commit e0ba3c26 authored by Mickaël Delahaye's avatar Mickaël Delahaye
Browse files

Change name to LAnnotate

parent f17c7800
FRAMAC_SHARE :=$(shell frama-c.byte -print-path)
FRAMAC_LIBDIR :=$(shell frama-c.byte -print-libpath)
PLUGIN_NAME = Genlabels
PLUGIN_NAME = LAnnotate
PLUGIN_TESTS_DIRS:=bubblesort
PLUGIN_CMO = options config utils annotators instru decision function register
include $(FRAMAC_SHARE)/Makefile.dynamic
GenLabels
LAnnotate
=========
GenLabels is a Frama-C plugin. It requires a patched version of Frama-C.
LAnnotate is a Frama-C plugin. It requires a patched version of Frama-C.
Installation
------------
......@@ -16,7 +16,7 @@ The former command may need to be run as root (or sudo) depending on your Frama-
Usage
-----
frama-c -genlabels=CRITERIA file.c
frama-c -lannot=CRITERIA file.c
where CRITERIA is a comma-separated list of criteria. It outputs a new annotated file named `file_labels.c`, with labels for each selected criterion.
......@@ -24,7 +24,7 @@ Implemented criteria are CC, MCC, WM, IDP, F and D.
### CC (Conditition Coverage)
frama-c -genlabels=CC file.c
frama-c -lannot=CC file.c
This command creates an annoted file with condition coverage labels only.
......@@ -44,7 +44,7 @@ Note that the second parameter of `pc_label` may vary, it's a unique identifier
### MCC (Multiple Condition Coverage)
frama-c -genlabels=MCC file.c
frama-c -lannot=MCC file.c
The following branch:
......@@ -60,12 +60,12 @@ becomes:
### WM (Weak Mutation)
frama-c -genlabels=WM file.c
frama-c -lannot=WM file.c
This command creates an annoted file with labels corresponding to every available mutators.
One can select more precisely mutators, like so:
frama-c -genlabels=WM -genlabels-mutators=AOR,COR file.c
frama-c -lannot=WM -lannot-mutators=AOR,COR file.c
Available mutators are ABS, AOR, COR and ROR.
......
include Plugin.Register (struct
let name = "GenLabels"
let shortname = "genlabels"
let name = "LAnnotate"
let shortname = "lannot"
let help = "generate labels"
end)
......@@ -13,15 +13,16 @@ let rec string_list l =
let annotators = ["MCC"; "CC"; "FC"; "DC"; "WM"; "IDP"]
module Annotators = StringSet (struct
let option_name = "-genlabels"
let option_name = "-lannot"
let arg_name = "criteria"
let help = "generate labels for each criterion (comma-separated list of criteria, among "^string_list annotators^")"
end)
let () = Annotators.set_possible_values annotators
let () = Annotators.add_aliases ["-lannotate"]
let mutators = ["AOR"; "ROR"; "COR"; "ABS"]
module Mutators = FilledStringSet (struct
let option_name = "-genlabels-mutators"
let option_name = "-lannot-mutators"
let arg_name = "mutators"
let help = "select mutators for WM labelling (comma-separated list of mutators among "^string_list mutators^", default: all)"
let default = Datatype.String.Set.of_list mutators
......@@ -31,14 +32,14 @@ let () = Mutators.set_possible_values mutators
let () = Plugin.argument_is_function_name ()
module FunctionNames = StringSet (struct
let arg_name = "funs"
let option_name = "-genlabels-functions"
let option_name = "-lannot-functions"
let help = "filter by function names (by default: disabled)"
end)
let () = Plugin.set_group help
let () = Plugin.do_not_journalize ()
module AnnotatorsHelp = False (struct
let option_name = "-genlabels-criteria-help"
let option_name = "-lannot-criteria-help"
let help = "show criteria help"
end)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment