-
Notifications
You must be signed in to change notification settings - Fork 2
/
action.yml
114 lines (114 loc) · 4.39 KB
/
action.yml
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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
name: 'Gobra'
description: 'Verify your Go project with Gobra'
inputs:
caching:
description: 'Enable caching of verification results. The possible values are 0 (disabled) and 1 (enabled).'
required: true
default: '1' # cache enabled by default
projectLocation:
description: 'Location in which the project is located in the workflow context. By default, it looks in a folder with the same name as the repository.'
required: false
includePaths:
description: 'Directories used for package lookup. Their paths are relative to the project location.'
required: false
files:
description: 'List of Go and Gobra files to verify.'
required: false
packages:
description: 'Names of the packages to verify. By default, all packages are verified.'
required: false
excludePackages:
description: 'Names of packages that should not be verified. This option takes precedence over the `package` option.'
required: false
recursive:
description: 'Verify nested packages recursively'
required: false
default: '0'
overflow:
description: 'Check for arithmetic overflows in integer expressions.'
required: false
default: '0'
chop:
description: 'Maximum number of files in which a file can be split with the chopper feature of Gobra. Larger values may improve the verification time of large codebases.'
default: '1'
viperBackend:
description: 'Which Viper backend to use. Can be one of "SILICON", "VSWITHSILICON", "CARBON", and "VSWITHCARBON".'
required: true
default: "VSWITHSILICON" # to allow caching by default
javaXss:
description: 'Java stack size. Should be increased in case of frequent stack overflows.'
required: true
default: '1g'
javaXmx:
description: 'Maximum size of the heap.'
required: true
default: '4g'
timeout:
description: 'Time-out for the verification job. Note that a GitHub workflow step times-out automatically after 6 hours.'
required: false
default: '6h'
imageName:
description: 'Base image of Gobra to be used.'
required: true
default: 'ghcr.io/viperproject/gobra'
imageVersion:
description: 'Version of the base image to be used.'
required: true
default: 'latest'
headerOnly:
description: 'Whether Gobra should only verify files with the header "// +gobra".'
required: false
default: '0'
module:
description: 'Name of current module that should be used for resolving imports.'
required: false
assumeInjectivityOnInhale:
description: 'Assume injectivity of the receiver expression when inhaling quantified permissions, instead of checking it, like in Viper versions previous to 2022.02.'
required: false
default: '1'
checkConsistency:
decription: 'Enforces additional consistency checks in the generated Viper code. Helpful to debug problems with the encoding of Gobra.'
required: false
default: '0'
mceMode:
description: 'Exhale Mode used together with a silicon-based backend. It can be enabled ("on"), disabled("off"), or enabled on demand ("od").'
required: false
default: 'on'
parallelizeBranches:
description: 'Parallelize branches in the silicon backend.'
required: false
default: '0'
requireTriggers:
description: 'Require that all quantifiers have user-provided triggers.'
required: false
default: '0'
conditionalizePermissions:
description: 'Tries to reduce the number of branches that Gobra has to deal with the option --conditionalizePermissions'
required: false
default: '0'
disableNL:
description: 'Disable non-linear integer arithmetic. Non compatible yet with Carbon'
required: false
default: '0'
moreJoins:
description: 'Specifies if silicon should be run with more joins completely enabled ("all"), disabled ("off"), or only for impure conditionals ("impure").'
required: false
default: 'off'
unsafeWildcardOptimization:
description: "Perform the optimization described in silicon's PR #756. You must ensure that the necessary conditions for the optimization are met."
required: false
default: '0'
useZ3API:
description: 'Use the Z3 API in silicon.'
required: false
default: '0'
statsFile:
description: 'Path where the generated stats.json file will be stored'
required: false
default: '/stats/'
outputs:
time:
description: 'Total verification time in seconds'
runs:
using: 'docker'
image: 'Dockerfile'