1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
include Plugin.Register
(struct
let name = "Region Analysis"
let help = "Memory Region Analysis (experimental)"
let shortname = "region"
end)
module Enabled = Action
(struct
let option_name = "-region"
let help = "Annotate all functions wrt regions"
end)
let () = Parameter_customize.set_negative_option_name "-region-check"
let () = Parameter_customize.set_negative_option_help "Generate ACSL 'check' annotations"
module Assert = False
(struct
let option_name = "-region-assert"
let help = "Generate ACSL 'assert' annotations instead of checks"
end)
module Logic = False
(struct
let option_name = "-region-logic"
let help = "Also generate guards for logic"
end)