diff options
| author | Christopher Pulte | 2015-11-06 10:35:08 +0000 |
|---|---|---|
| committer | Christopher Pulte | 2015-11-06 10:35:08 +0000 |
| commit | b06d3a59c74c7e1347c49665a9d399dd411d1c84 (patch) | |
| tree | fdc678603bbec18a285b392a57100f6e4d5ffdde /src/spec_analysis.mli | |
| parent | 5a33d9f5ec9fae7336933f34363e0eee246242b8 (diff) | |
fixes
Diffstat (limited to 'src/spec_analysis.mli')
| -rw-r--r-- | src/spec_analysis.mli | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli index 94698954..1b1197dd 100644 --- a/src/spec_analysis.mli +++ b/src/spec_analysis.mli @@ -5,4 +5,15 @@ open Type_internal type typ = Type_internal.t +(*Returns the declared default order of a set of definitions, defaulting to Inc if no default is provided *) val default_order : tannot defs -> order + +(*Determines if the first typ is within the range of the the second typ, + using the constraints provided when the first typ contains variables. + It is an error for second typ to be anything other than a range type + If the first typ is a vector, then determines if the max representable + number is in the range of the second; it is an error for the first typ + to be anything other than a vector, a range, an atom, or a bit (after + suitable unwrapping of abbreviations, reg, and registers). +*) +val is_within_range: typ -> typ -> nexp_range list -> triple |