Legend:
Library
Module
Module type
Parameter
Class
Class type
Assembly instruction.
On a high level, the instruction is a pair of the opcode and operands. A BIL code, that describes semantics of the instruction may be attached to it. Also, semantic tags (or flags) may add further information about the instruction.
The instruction are usually created by a low level machinery, and analyzed on the later stages. So, usually, there is no need to create one manually.
For example, each block is a sequence of instructions (see Block.insns), also with each non-synthetic term there is an an Disasm.insn field, that stores an instruction from which the term was born.
type t = Bap_core_theory.Theory.Program.Semantics.t
includeCore_kernel.Bin_prot.Binable.S withtypet := t
includePpx_sexp_conv_lib.Sexpable.S withtypet := t
A property or a semantic tag is some kind of attribute associated with an instruction. Usually a property is a boolean, it either holds or not. In our case we employ modular logic, and a property can have an intermediate state between true and false. That means, that we have two kinds of relations, strong "must" and weaker "may". The must property is known to be a property associated with the instruction. It is a strong knowledge. For example, if an instruction has jump property, then it is guaranteed to be a jump instruction. On the other hand, the may property represent some uncertain knowledge. For example, the load property is may as it designates that an instruction may access the main memory, or may not access, as it depends on some information, that cannot be deduced statically.