Make (p.codex.1.0~rc4.doc.codex.terms.Terms.Const

The Codex static analysis library
- Quick start: verifying C code using Frama-C/Codex
- Tutorials
- Spatial Memory Safety with Dependent Types in Codex
- Extending Codex to a simple while language
- Overview: The While Language
- Lattices and Single Value Abstractions
- Interval Analysis on While Language
- Interval Analysis using Codex
- Library Type_parser
  - Type_parser
- Library codex
  - Codex
- Library codex.bdd
  - Bdd
- Library codex.binarytrace
  - Binarytrace
- Library codex.cfg
  - Cfg
- Library codex.codex_config
  - Codex_config
- Library codex.codex_log
  - Codex_log
- Library codex.compressor
  - Compressor
- Library codex.condition_map
  - Condition_map
- Library codex.datatype_sig
  - Datatype_sig
- Library codex.domains
  - Domains
- Library codex.emit_alarm
  - Emit_alarm
- Library codex.extstdlib
  - Extstdlib
- Library codex.file_to_html
  - File_to_html
- Library codex.fixpoint
  - Fixpoint
- Library codex.framac_ival
  - Framac_ival
- Library codex.gui
  - Gui
- Library codex.hashing
  - Hashing
- Library codex.het-hashtbl
  - HetHashtbl
- Library codex.hook
  - Hook
- Library codex.int_builtins
  - Int_builtins
- Library codex.interval_map
  - Interval_map
- Library codex.lattices
  - Lattices
- Library codex.online_nearest_common_ancestor_skiplist
  - Online_nearest_common_ancestor_skiplist
- Library codex.operator
  - Operator
- Library codex.record_time
  - Record_time
- Library codex.single_value_abstraction
  - Single_value_abstraction
- Library codex.smallmap
  - Smallmap
- Library codex.smtbackend
  - Smtbackend
- Library codex.stats
  - Stats
- Library codex.syntax_tree
  - Syntax_tree
- Library codex.terms
  - Terms
- Library codex.tracelog
  - Tracelog
- Library codex.treemap
  - Treemap
- Library codex.types
  - Types
- Library codex.union_find
  - Union_Find
- Library codex.units
  - Units
- Library codex.utils
- Library codex.while_ast
  - While_ast
- Library codex.whilelib
  - Whilelib
- Library immutable_array
  - Immutable_array
- Library interface
  - Interface
- Library ppx_while
  - Ppx_while
- Library type_parse_tree
  - Type_parse_tree
- Sources

Parameters

module Terms : Sig.TERMS

Signature

Sourceexception Empty

Sourceexception Not_a_constant

Returns the value if the term is indeed a singleton value;

raises Empty
if it is the empty value;

raises Not_a_constant
if it is not constant.

Sourceval integer : Operator.Function_symbol.integer Terms.t -> Z.t

Sourceval boolean : Operator.Function_symbol.boolean Terms.t -> bool

Sourceval binary : Operator.Function_symbol.binary Terms.t -> Z.t

Sourceval bitvector : Operator.Function_symbol.bitvector Terms.t -> Z.t

Sourceval enum : Operator.Function_symbol.enum Terms.t -> Z.t